diff options
Diffstat (limited to 'user-contrib/Ltac2/tac2entries.mli')
| -rw-r--r-- | user-contrib/Ltac2/tac2entries.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli index e02c126e71..273cf02c9b 100644 --- a/user-contrib/Ltac2/tac2entries.mli +++ b/user-contrib/Ltac2/tac2entries.mli @@ -23,13 +23,14 @@ val register_primitive : ?local:bool -> val register_struct : ?local:bool - -> pstate:Proof_global.pstate option -> strexpr -> unit val register_notation : ?local:bool -> sexpr list -> int option -> raw_tacexpr -> unit +val perform_eval : pstate:Proof_global.pstate option -> raw_tacexpr -> unit + (** {5 Notations} *) type scope_rule = @@ -50,7 +51,7 @@ val print_ltac : Libnames.qualid -> unit (** {5 Eval loop} *) (** Evaluate a tactic expression in the current environment *) -val call : pstate:Proof_global.t -> default:bool -> raw_tacexpr -> Proof_global.t +val call : pstate:Proof_global.pstate -> default:bool -> raw_tacexpr -> Proof_global.pstate (** {5 Toplevel exceptions} *) |