From e3c247c1d96f39d2c07d120b69598a904b7d9f19 Mon Sep 17 00:00:00 2001 From: Matej Košík Date: Sun, 11 Jun 2017 15:14:15 +0200 Subject: deprecate Pp.std_ppcmds type alias --- proofs/refiner.mli | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'proofs/refiner.mli') diff --git a/proofs/refiner.mli b/proofs/refiner.mli index aac10e81b..3ff010fe3 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -31,7 +31,7 @@ val refiner : rule -> tactic (** [tclIDTAC] is the identity tactic without message printing*) val tclIDTAC : tactic -val tclIDTAC_MESSAGE : Pp.std_ppcmds -> tactic +val tclIDTAC_MESSAGE : Pp.t -> tactic (** [tclEVARS sigma] changes the current evar map *) val tclEVARS : evar_map -> tactic @@ -100,7 +100,7 @@ val tclTHENLASTn : tactic -> tactic array -> tactic val tclTHENFIRSTn : tactic -> tactic array -> tactic (** A special exception for levels for the Fail tactic *) -exception FailError of int * Pp.std_ppcmds Lazy.t +exception FailError of int * Pp.t Lazy.t (** Takes an exception and either raise it at the next level or do nothing. *) @@ -116,8 +116,8 @@ val tclTRY : tactic -> tactic val tclTHENTRY : tactic -> tactic -> tactic val tclCOMPLETE : tactic -> tactic val tclAT_LEAST_ONCE : tactic -> tactic -val tclFAIL : int -> Pp.std_ppcmds -> tactic -val tclFAIL_lazy : int -> Pp.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 -- cgit v1.2.3