Merge pull request #1005 from SkySkimmer/let-abstract

Adapt to coq/coq#17576 (declare_variable takes typing flags argument)
MetaCoq · Nov 4, 2023 · f593f01 · f593f01
2 parents 64ce785 + 67cd5e9
commit f593f01
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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) ->