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 --- tactics/class_tactics.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tactics/class_tactics.ml') diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 6cc9d3d55..72e57a85b 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -621,7 +621,7 @@ module V85 = struct type autoinfo = { hints : hint_db; is_evar: existential_key option; only_classes: bool; unique : bool; - auto_depth: int list; auto_last_tac: std_ppcmds Lazy.t; + auto_depth: int list; auto_last_tac: Pp.t Lazy.t; auto_path : global_reference option list; auto_cut : hints_path } type autogoal = goal * autoinfo @@ -972,7 +972,7 @@ end module Search = struct type autoinfo = { search_depth : int list; - last_tac : Pp.std_ppcmds Lazy.t; + last_tac : Pp.t Lazy.t; search_dep : bool; search_only_classes : bool; search_cut : hints_path; -- cgit v1.2.3