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.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs/refiner.ml') diff --git a/proofs/refiner.ml b/proofs/refiner.ml index f1b1cd359..3e3313eb5 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -63,7 +63,7 @@ let tclIDTAC_MESSAGE s gls = let tclFAIL_s s gls = user_err ~hdr:"Refiner.tclFAIL_s" (str s) (* A special exception for levels for the Fail tactic *) -exception FailError of int * std_ppcmds Lazy.t +exception FailError of int * Pp.t Lazy.t (* The Fail tactic *) let tclFAIL lvl s g = raise (FailError (lvl,lazy s)) -- cgit v1.2.3