From bd75d655c86e8ddf1fc92663525c755c500cb39c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 3 Mar 2025 15:38:20 +0100 Subject: [PATCH] Adapt to coq/coq#20313 (wit_tactic does not handle ltac in term) --- src/rocq_elpi_builtins.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/rocq_elpi_builtins.ml b/src/rocq_elpi_builtins.ml index 7ceb691ec..8af81635d 100644 --- a/src/rocq_elpi_builtins.ml +++ b/src/rocq_elpi_builtins.ml @@ -977,7 +977,7 @@ let cache_abbrev_for_tac { abbrev_name; tac_name = tacname; tac_fixed_args = mor let args = args |> List.map (fun (arg,_) -> Rocq_elpi_arg_HOAS.Tac.Term(arg)) in let args = Genarg.in_gen (Genarg.rawwit (Genarg.wit_list Rocq_elpi_arg_syntax.wit_elpi_tactic_arg)) (more_args @ args) in (TacML (elpi_tac_entry, [TacGeneric(None, tacname); TacGeneric(None, args)])) in - CAst.make @@ Constrexpr.CGenarg (Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) (CAst.make tac)) in + CAst.make @@ Constrexpr.CGenarg (Genarg.in_gen (Genarg.rawwit Tacarg.wit_ltac_in_term) (CAst.make tac)) in let Gbpmp (rule, action) = gbpmp action (List.rev abbrev_name) in Pcoq.grammar_extend Pcoq.Constr.term (Pcoq.Fresh (Gramlib.Gramext.Before "10",