Removing compatibility layers related to printing.

4 files changed, 12 insertions, 15 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 2f8af6b44..84ca0aa8f 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
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 9e9635e8a..2446b6996 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -792,7 +792,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
 	else begin
 	  if not eapply then failwith "make_apply_entry";
           if verbose then
-	    Feedback.msg_info (str "the hint: eapply " ++ pr_lconstr (EConstr.Unsafe.to_constr c) ++
+	    Feedback.msg_info (str "the hint: eapply " ++ pr_leconstr_env env sigma' c ++
 	    str " will only be used by eauto");
           (Some hd,
            { pri = (match pri with None -> nb_hyp sigma' cty + nmiss | Some p -> p);
@@ -813,7 +813,7 @@ let pr_hint_term env sigma ctx = function
   | IsGlobRef gr -> pr_global gr
   | IsConstr (c, ctx) ->
      let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
-     pr_constr_env env sigma (EConstr.Unsafe.to_constr c)
+     pr_econstr_env env sigma c
 
 (** We need an object to record the side-effect of registering
   global universes associated with a hint. *)
@@ -863,7 +863,7 @@ let make_resolves env sigma flags pri poly ?name cr =
   in
   if List.is_empty ents then
     user_err ~hdr:"Hint"
-      (pr_lconstr (EConstr.Unsafe.to_constr c) ++ spc() ++
+      (pr_leconstr_env env sigma c ++ spc() ++
         (if pi1 flags then str"cannot be used as a hint."
 	else str "can be used as a hint only for eauto."));
   ents
@@ -1360,7 +1360,7 @@ let make_db_list dbnames =
 (*                    Functions for printing the hints                    *)
 (**************************************************************************)
 
-let pr_hint_elt (c, _, _) = pr_constr (EConstr.Unsafe.to_constr c)
+let pr_hint_elt (c, _, _) = pr_econstr c
 
 let pr_hint h = match h.obj with
   | Res_pf (c, _) -> (str"simple apply " ++ pr_hint_elt c)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index ef3bfc9d0..2d59285e6 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -42,7 +42,7 @@ let nlocal_def (na, b, t) =
 
 let no_inductive_inconstr env sigma constr =
   (str "Cannot recognize an inductive predicate in " ++
-     pr_lconstr_env env sigma (EConstr.Unsafe.to_constr constr) ++
+     pr_leconstr_env env sigma constr ++
      str "." ++ spc () ++ str "If there is one, may be the structure of the arity" ++
      spc () ++ str "or of the type of constructors" ++ spc () ++
      str "is hidden by constant definitions.")
@@ -277,14 +277,12 @@ let lemInv id c gls =
     Proofview.V82.of_tactic (Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false) gls
   with
     | NoSuchBinding ->
-        let c = EConstr.Unsafe.to_constr c in
 	user_err 
-	  (hov 0 (pr_constr c ++ spc () ++ str "does not refer to an inversion lemma."))
+	  (hov 0 (pr_econstr_env (Refiner.pf_env gls) (Refiner.project gls) c ++ spc () ++ str "does not refer to an inversion lemma."))
     | UserError (a,b) ->
-        let c = EConstr.Unsafe.to_constr c in
 	 user_err ~hdr:"LemInv"
 	   (str "Cannot refine current goal with the lemma " ++
-	      pr_lconstr_env (Refiner.pf_env gls) (Refiner.project gls) c)
+	      pr_leconstr_env (Refiner.pf_env gls) (Refiner.project gls) c)
 
 let lemInv_gen id c = try_intros_until (fun id -> Proofview.V82.tactic (lemInv id c)) id
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4e833eb55..dcaa15fd8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3073,7 +3073,7 @@ let warn_unused_intro_pattern =
           strbrk"Unused introduction " ++ str (String.plural (List.length names) "pattern")
           ++ str": " ++ prlist_with_sep spc 
          (Miscprint.pr_intro_pattern 
-	 (fun c -> Printer.pr_constr (EConstr.Unsafe.to_constr (fst (run_delayed (Global.env()) Evd.empty c))))) names)
+	 (fun c -> Printer.pr_econstr (fst (run_delayed (Global.env()) Evd.empty c)))) names)
 
 let check_unused_names names =
   if not (List.is_empty names) && Flags.is_verbose () then