diff options
| author |  Matej Košík <matej.kosik@inria.fr> | 2017-06-11 15:14:15 +0200 |
|---|---|---|
| committer | Matej Košík <matej.kosik@inria.fr> | 2017-07-27 10:10:23 +0200 |
| commit | e3c247c1d96f39d2c07d120b69598a904b7d9f19 (patch) | |
| tree | a9d3735d5d3f53140aa1123e87f4d4c8db8840f8 /tactics/tacticals.mli | |
| parent | a960c4db9ae93a6445f9db620f96f62b397ba8b5 (diff) | |
deprecate Pp.std_ppcmds type alias
Diffstat (limited to 'tactics/tacticals.mli')
| -rw-r--r-- | tactics/tacticals.mli | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 4ad9c6541..2a04c413b 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Names open Term open EConstr @@ -19,7 +18,7 @@ open Tactypes (** Tacticals i.e. functions from tactics to tactics. *) val tclIDTAC : tactic -val tclIDTAC_MESSAGE : std_ppcmds -> tactic +val tclIDTAC_MESSAGE : Pp.t -> tactic val tclORELSE0 : tactic -> tactic -> tactic val tclORELSE : tactic -> tactic -> tactic val tclTHEN : tactic -> tactic -> tactic @@ -41,8 +40,8 @@ val tclSOLVE : tactic list -> tactic val tclTRY : tactic -> tactic val tclCOMPLETE : tactic -> tactic val tclAT_LEAST_ONCE : tactic -> tactic -val tclFAIL : int -> std_ppcmds -> tactic -val tclFAIL_lazy : int -> std_ppcmds Lazy.t -> tactic +val tclFAIL : int -> Pp.t -> tactic +val tclFAIL_lazy : int -> Pp.t Lazy.t -> tactic val tclDO : int -> tactic -> tactic val tclPROGRESS : tactic -> tactic val tclSHOWHYPS : tactic -> tactic @@ -160,9 +159,9 @@ module New : sig (* [tclFAIL n msg] fails with [msg] as an error message at level [n] (meaning that it will jump over [n] error catching tacticals FROM THIS MODULE. *) - val tclFAIL : int -> Pp.std_ppcmds -> 'a tactic + val tclFAIL : int -> Pp.t -> 'a tactic - val tclZEROMSG : ?loc:Loc.t -> Pp.std_ppcmds -> 'a tactic + val tclZEROMSG : ?loc:Loc.t -> Pp.t -> 'a tactic (** Fail with a [User_Error] containing the given message. *) val tclOR : unit tactic -> unit tactic -> unit tactic |