diff --git a/builtin-doc/coq-builtin.elpi b/builtin-doc/coq-builtin.elpi index a6a858b95..4d62b1f8b 100644 --- a/builtin-doc/coq-builtin.elpi +++ b/builtin-doc/coq-builtin.elpi @@ -1619,6 +1619,11 @@ external pred coq.ltac.collect-goals i:term, o:list sealed-goal, % of type ltac1-tactic, see the tac argument constructor % and the ltac_tactic:(...) syntax to pass arguments to % an elpi tactic. +% Caveat: +% if Tac is a tactic name, then the tactic must be defined using +% "Ltac name := body", it cannot be a builtin one. For example +% "Ltac myapply x := apply x." lets one call apply by running +% coq.ltac.call-ltac1 "myapply" G GL. % Supported attributes: % - @no-tc! (default false, do not infer typeclasses) external pred coq.ltac.call-ltac1 i:any, i:goal, o:list sealed-goal. diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index f62085953..a1d3dd73a 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -3709,6 +3709,11 @@ Tac can either be a string (the tactic name), or a value of type ltac1-tactic, see the tac argument constructor and the ltac_tactic:(...) syntax to pass arguments to an elpi tactic. +Caveat: + if Tac is a tactic name, then the tactic must be defined using + "Ltac name := body", it cannot be a builtin one. For example + "Ltac myapply x := apply x." lets one call apply by running + coq.ltac.call-ltac1 "myapply" G GL. Supported attributes: - @no-tc! (default false, do not infer typeclasses)|})))), (fun tac (proof_context,goal,tac_args) _ ~depth _ _ -> abstract__grab_global_env_keep_sigma "coq.ltac.call-ltac1" (fun state ->