Skip to content

Commit

Permalink
Remove kludge
Browse files Browse the repository at this point in the history
  • Loading branch information
@JasonGross
JasonGross committed Apr 6, 2023
1 parent 397c501 commit 5e7b80e
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion quotation/theories/CommonUtils.v
View file
Original file line number Diff line number Diff line change
@@ -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.
Expand Down

0 comments on commit 5e7b80e

Please sign in to comment.