From 67cd5e957686a4db0d1419139926aa53e95d511f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 2 Nov 2023 15:28:54 +0100 Subject: [PATCH] Adapt to coq/coq#17576 (declare_variable takes typing flags argument) --- template-coq/src/run_template_monad.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/template-coq/src/run_template_monad.ml b/template-coq/src/run_template_monad.ml index 681adb262..612804821 100644 --- a/template-coq/src/run_template_monad.ml +++ b/template-coq/src/run_template_monad.ml @@ -355,7 +355,7 @@ let rec run_template_program_rec ~poly ?(intactic=false) (k : Constr.t Plugin_co let kind = Decls.IsAssumption Decls.Definitional in (* FIXME: better handling of evm *) let empty_mono_univ_entry = UState.Monomorphic_entry Univ.ContextSet.empty, UnivNames.empty_binders in - Declare.declare_variable ~name ~kind ~typ ~impl:Glob_term.Explicit ~univs:empty_mono_univ_entry; + Declare.declare_variable ~typing_flags:None ~name ~kind ~typ ~impl:Glob_term.Explicit ~univs:empty_mono_univ_entry; let env = Global.env () in k ~st env evm (Lazy.force unit_tt) | TmDefinition (opaque,name,s,typ,body) ->