Remove kludge

JasonGross · JasonGross · commit 0bff5bf19ee7 · 2023-04-06T23:37:58.000-07:00
diff --git a/quotation/theories/CommonUtils.v b/quotation/theories/CommonUtils.v
@@ -1,4 +1,3 @@
-From MetaCoq.Template Require TypingWf. (* Kludge to avoid universe inconsistencies that arise when this file is required later, things like Error: Universe inconsistency. Cannot enforce Coq.Init.Datatypes.26 < replace_quotation_of.u0 because replace_quotation_of.u0 <= MetaCoq.Template.MonadAst.6 <= prod.u0 = Coq.Init.Datatypes.26. *)
 From MetaCoq.Utils Require Import utils monad_utils MCList.
 From MetaCoq.Common Require Import Kernames MonadBasicAst.
 From MetaCoq.Template Require MonadAst TemplateMonad Ast Loader.

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,3 @@`
`1`		`-From MetaCoq.Template Require TypingWf. (* Kludge to avoid universe inconsistencies that arise when this file is required later, things like Error: Universe inconsistency. Cannot enforce Coq.Init.Datatypes.26 < replace_quotation_of.u0 because replace_quotation_of.u0 <= MetaCoq.Template.MonadAst.6 <= prod.u0 = Coq.Init.Datatypes.26. *)`
`2`	`1`	`From MetaCoq.Utils Require Import utils monad_utils MCList.`
`3`	`2`	`From MetaCoq.Common Require Import Kernames MonadBasicAst.`
`4`	`3`	`From MetaCoq.Template Require MonadAst TemplateMonad Ast Loader.`