diff options
| author | Gaëtan Gilbert | 2020-10-09 21:56:24 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-10-26 14:42:15 +0100 |
| commit | 30f97beb1bfc149d9608cb74f24f69f268671e04 (patch) | |
| tree | 7423e52ead0509a4496fc40741664867d26db2ed /user-contrib/Ltac2/tac2entries.mli | |
| parent | 5146b2f01b3b901ac99823d3a448c77560f248db (diff) | |
Ltac2: use ComTactic infrastructure
Diffstat (limited to 'user-contrib/Ltac2/tac2entries.mli')
| -rw-r--r-- | user-contrib/Ltac2/tac2entries.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli index fc56a54e3a..2f053df2d0 100644 --- a/user-contrib/Ltac2/tac2entries.mli +++ b/user-contrib/Ltac2/tac2entries.mli @@ -53,7 +53,7 @@ val print_ltac : Libnames.qualid -> unit (** {5 Eval loop} *) (** Evaluate a tactic expression in the current environment *) -val call : pstate:Declare.Proof.t -> default:bool -> raw_tacexpr -> Declare.Proof.t +val call : pstate:Declare.Proof.t -> with_end_tac:bool -> raw_tacexpr -> Declare.Proof.t (** {5 Toplevel exceptions} *) |