diff options
| author | Pierre-Marie Pédrot | 2016-11-25 11:36:09 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:30:39 +0100 |
| commit | 778e863b77bcafc8ed339dd02226e85e5fee2532 (patch) | |
| tree | c836854265a6c1ac401b524710a0b7947bea3d37 /tactics/class_tactics.ml | |
| parent | 05afd04095e35d77ca135bd2c1cb8d303ea2d6a8 (diff) | |
Removing compatibility layers related to printing.
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 2f8af6b449..84ca0aa8f2 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -185,8 +185,7 @@ let set_typeclasses_depth = optwrite = set_typeclasses_depth; } let pr_ev evs ev = - Printer.pr_constr_env (Goal.V82.env evs ev) evs - (Evarutil.nf_evar evs (EConstr.Unsafe.to_constr (Goal.V82.concl evs ev))) + Printer.pr_econstr_env (Goal.V82.env evs ev) evs (Goal.V82.concl evs ev) (** Typeclasses instance search tactic / eauto *) @@ -764,7 +763,7 @@ module V85 = struct if foundone == None && !typeclasses_debug > 0 then Feedback.msg_debug (pr_depth info.auto_depth ++ str": no match for " ++ - Printer.pr_constr_env (Goal.V82.env s gl) s (EConstr.Unsafe.to_constr concl) ++ + Printer.pr_econstr_env (Goal.V82.env s gl) s concl ++ spc () ++ str ", " ++ int (List.length poss) ++ str" possibilities"); match foundone with @@ -1005,7 +1004,7 @@ module Search = struct if !typeclasses_debug > 0 then Feedback.msg_debug (pr_depth info.search_depth ++ str": looking for " ++ - Printer.pr_constr_env (Goal.env gl) s (EConstr.Unsafe.to_constr concl) ++ + Printer.pr_econstr_env (Goal.env gl) s concl ++ (if backtrack then str" with backtracking" else str" without backtracking")); let secvars = compute_secvars gl in @@ -1120,7 +1119,7 @@ module Search = struct if !foundone == false && !typeclasses_debug > 0 then Feedback.msg_debug (pr_depth info.search_depth ++ str": no match for " ++ - Printer.pr_constr_env (Goal.env gl) s (EConstr.Unsafe.to_constr concl) ++ + Printer.pr_econstr_env (Goal.env gl) s concl ++ spc () ++ str ", " ++ int (List.length poss) ++ str" possibilities"); match e with |