Adapt to coq/coq#17576 (declare_variable takes typing flags argument)

MetaCoq · Nov 2, 2023 · 67cd5e9 · 67cd5e9
1 parent 64ce785
commit 67cd5e9
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) ->