diff options
| author | Gaëtan Gilbert | 2019-05-20 17:11:00 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-06-04 13:58:42 +0200 |
| commit | 99154fcb97653c606d2e62e0a0521c4afddff44c (patch) | |
| tree | 4e8fed2571d370acdc486f486e847a6317d60f69 /user-contrib/Ltac2 | |
| parent | 1ea1e218eed9792685bd7467b63a17fb5ebdbb7e (diff) | |
Rename Proof_global.{pstate -> t}
Diffstat (limited to 'user-contrib/Ltac2')
| -rw-r--r-- | user-contrib/Ltac2/tac2entries.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli index 273cf02c9b..80d48f67ba 100644 --- a/user-contrib/Ltac2/tac2entries.mli +++ b/user-contrib/Ltac2/tac2entries.mli @@ -29,7 +29,7 @@ val register_struct val register_notation : ?local:bool -> sexpr list -> int option -> raw_tacexpr -> unit -val perform_eval : pstate:Proof_global.pstate option -> raw_tacexpr -> unit +val perform_eval : pstate:Proof_global.t option -> raw_tacexpr -> unit (** {5 Notations} *) @@ -51,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.pstate -> default:bool -> raw_tacexpr -> Proof_global.pstate +val call : pstate:Proof_global.t -> default:bool -> raw_tacexpr -> Proof_global.t (** {5 Toplevel exceptions} *) |