Ltac now uses evar-based constrs.

1 files changed, 7 insertions, 7 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 8290ca945..04aacdc09 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -70,10 +70,10 @@ let ppwf_paths x = pp (Rtree.pp_tree pprecarg x)
 (* term printers *)
 let rawdebug = ref false
 let ppevar evk = pp (str (Evd.string_of_existential evk))
-let ppconstr x = pp (Termops.print_constr x)
-let ppeconstr x = pp (Termops.print_constr (EConstr.Unsafe.to_constr x))
+let ppconstr x = pp (Termops.print_constr (EConstr.of_constr x))
+let ppeconstr x = pp (Termops.print_constr x)
 let ppconstr_expr x = pp (Ppconstr.pr_constr_expr x)
-let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr x)
+let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr (EConstr.of_constr x))
 let ppterm = ppconstr
 let ppsconstr x = ppconstr (Mod_subst.force_constr x)
 let ppconstr_univ x = Constrextern.with_universes ppconstr x
@@ -98,9 +98,9 @@ let ppidmap pr l = pp (pridmap pr l)
 
 let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) ->
   hov 0
-  (Termops.print_constr c ++
+  (Termops.print_constr (EConstr.of_constr c) ++
    (match copt with None -> mt () | Some c -> spc () ++ str "<expanded: " ++
-    Termops.print_constr c ++ str">") ++
+    Termops.print_constr (EConstr.of_constr c) ++ str">") ++
    (if id = id0 then mt ()
     else spc () ++ str "<canonical: " ++ pr_id id ++ str ">"))))
 
@@ -109,7 +109,7 @@ let ppididmap = ppidmap (fun _ -> pr_id)
 
 let prconstrunderbindersidmap = pridmap (fun _ (l,c) ->
   hov 1 (str"[" ++  prlist_with_sep spc Id.print l ++ str"]")
-  ++ str "," ++ spc () ++ Termops.print_constr (EConstr.Unsafe.to_constr c))
+  ++ str "," ++ spc () ++ Termops.print_constr c)
 
 let ppconstrunderbindersidmap l = pp (prconstrunderbindersidmap l)
 
@@ -159,7 +159,7 @@ let prdelta s = pp (Mod_subst.debug_pr_delta s)
 let pp_idpred s = pp (pr_idpred s)
 let pp_cpred s = pp (pr_cpred s)
 let pp_transparent_state s = pp (pr_transparent_state s)
-let pp_stack_t n = pp (Reductionops.Stack.pr Termops.print_constr n)
+let pp_stack_t n = pp (Reductionops.Stack.pr (EConstr.of_constr %> Termops.print_constr) n)
 let pp_cst_stack_t n = pp (Reductionops.Cst_stack.pr n)
 let pp_state_t n = pp (Reductionops.pr_state n)