From 5e7b80e3593490d99853acf849d8e619058c522e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 4 Apr 2023 23:02:55 -0700 Subject: [PATCH] Remove kludge --- quotation/theories/CommonUtils.v | 1 - 1 file changed, 1 deletion(-) diff --git a/quotation/theories/CommonUtils.v b/quotation/theories/CommonUtils.v index 0e0e12cf2c..1f7fd3435f 100644 --- 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.