Skip to content

Commit d453e00

Browse files
committed
typo
1 parent 7fc2598 commit d453e00

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/rocq_elpi_builtins.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4110,7 +4110,7 @@ starts from 0. Also, each block has a name, "Lia" in this case.
41104110

41114111
Supported attributes:
41124112
- @no-tc! (default false, do not infer typeclasses)|})))))),
4113-
(fun plugin block index (proof_context,goal,tac_args) _ ~depth _ _ -> abstract__grab_global_env_keep_sigma "coq.ltac.call-ltac1" (fun state ->
4113+
(fun plugin block index (proof_context,goal,tac_args) _ ~depth _ _ -> abstract__grab_global_env_keep_sigma "coq.ltac.call-mltac" (fun state ->
41144114
let no_tc = if proof_context.options.no_tc = Some true then true else false in
41154115
let open Ltac_plugin in
41164116

0 commit comments

Comments
 (0)