Merge pull request #835 from SkySkimmer/pgenarg

Adapt to coq/coq#17220 (genargs are not holes)
MetaCoq · Feb 10, 2023 · 558a314 · 558a314
2 parents 84f41d7 + 3358c3d
commit 558a314
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/template-coq/src/plugin_core.ml b/template-coq/src/plugin_core.ml
@@ -111,7 +111,7 @@ let tmAxiom (nm : ident) ?poly:(poly=false) (typ : term) : kername tm =
 let tmLemma (nm : ident) ?poly:(poly=false)(ty : term) : kername tm =
   fun ~st env evm success _fail ->
     let kind = Decls.(IsDefinition Definition) in
-    let hole = CAst.make (Constrexpr.CHole (Some Evar_kinds.(QuestionMark default_question_mark), Namegen.IntroAnonymous, None)) in
+    let hole = CAst.make (Constrexpr.CHole (Some Evar_kinds.(QuestionMark default_question_mark), Namegen.IntroAnonymous)) in
     Feedback.msg_debug (Pp.str "interp_casted called");
     let evm, (c, _) =
       try Constrintern.interp_casted_constr_evars_impls ~program_mode:true env evm hole (EConstr.of_constr ty)

diff --git a/template-coq/src/run_template_monad.ml b/template-coq/src/run_template_monad.ml
@@ -415,7 +415,7 @@ let rec run_template_program_rec ~poly ?(intactic=false) (k : Constr.t Plugin_co
   | TmLemma (name,typ) ->
     let name = reduce_all env evm name in
     let kind = Decls.(IsDefinition Definition) in
-    let hole = CAst.make (Constrexpr.CHole (None, Namegen.IntroAnonymous, None)) in
+    let hole = CAst.make (Constrexpr.CHole (None, Namegen.IntroAnonymous)) in
     let evm, (c, _) = Constrintern.interp_casted_constr_evars_impls ~program_mode:true env evm hole (EConstr.of_constr typ) in
     let ident = unquote_ident name in
     RetrieveObl.check_evars env evm;