Ltac now uses evar-based constrs.

7 files changed, 13 insertions, 15 deletions

diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index d4b46c046..875e4a118 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -208,6 +208,6 @@ let split_tycon loc env evd tycon =
 let valcon_of_tycon x = x
 let lift_tycon n = Option.map (lift n)
 
-let pr_tycon env = function
+let pr_tycon env sigma = function
     None -> str "None"
-  | Some t -> Termops.print_constr_env env (EConstr.Unsafe.to_constr t)
+  | Some t -> Termops.print_constr_env env sigma t
diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli
index 9c03a6e3f..2f7ac4efb 100644
--- a/pretyping/evardefine.mli
+++ b/pretyping/evardefine.mli
@@ -43,5 +43,5 @@ val define_evar_as_sort : env -> evar_map -> existential -> evar_map * sorts
 
 (** {6 debug pretty-printer:} *)
 
-val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
+val pr_tycon : env -> evar_map -> type_constraint -> Pp.std_ppcmds
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a0d8faab4..09b99983c 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -429,7 +429,7 @@ let protected_get_type_of env sigma c =
   try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c
   with Retyping.RetypeError _ ->
     user_err 
-      (str "Cannot reinterpret " ++ quote (print_constr (EConstr.Unsafe.to_constr c)) ++
+      (str "Cannot reinterpret " ++ quote (print_constr c) ++
        str " in the current environment.")
 
 let pretype_id pretype k0 loc env evdref lvar id =
@@ -1225,6 +1225,7 @@ let type_uconstr ?(flags = constr_flags)
   } in
   let sigma = Sigma.to_evar_map sigma in
   let (sigma, c) = understand_ltac flags env sigma vars expected_type term in
+  let c = EConstr.of_constr c in
   Sigma.Unsafe.of_pair (c, sigma)
   end }
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 2f3ce3afa..a1602088a 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -119,7 +119,7 @@ val understand_judgment_tcc : env -> evar_map ref ->
 val type_uconstr :
   ?flags:inference_flags ->
   ?expected_type:typing_constraint ->
-  Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr Tactypes.delayed_open
+  Geninterp.interp_sign -> Glob_term.closed_glob_constr -> EConstr.constr Tactypes.delayed_open
 
 (** Trying to solve remaining evars and remaining conversion problems
     possibly using type classes, heuristics, external tactic solver
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 8362a2a26..bc9e3a1f4 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -191,7 +191,7 @@ let warn_projection_no_head_constant =
   CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker"
          (fun (t,con_pp,proji_sp_pp) ->
           strbrk "Projection value has no head constant: "
-          ++ Termops.print_constr t ++ strbrk " in canonical instance "  
+          ++ Termops.print_constr (EConstr.of_constr t) ++ strbrk " in canonical instance "  
           ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")
 
 (* Intended to always succeed *)
@@ -256,8 +256,8 @@ let add_canonical_structure warn o =
       in match ocs with
         | None -> object_table := Refmap.add proj ((pat,s)::l) !object_table;
         | Some (c, cs) ->
-              let old_can_s = (Termops.print_constr cs.o_DEF)
-              and new_can_s = (Termops.print_constr s.o_DEF) in
+              let old_can_s = (Termops.print_constr (EConstr.of_constr cs.o_DEF))
+              and new_can_s = (Termops.print_constr (EConstr.of_constr s.o_DEF)) in
               let prj = (Nametab.pr_global_env Id.Set.empty proj)
               and hd_val = (pr_cs_pattern cs_pat) in
               if warn then warn_redundant_canonical_projection (hd_val,prj,new_can_s,old_can_s))
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 90c5b241b..bc5c629f4 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -210,7 +210,7 @@ module Cst_stack = struct
 
   let pr l =
     let open Pp in
-    let p_c c = Termops.print_constr (EConstr.Unsafe.to_constr c) in
+    let p_c c = Termops.print_constr c in
     prlist_with_sep pr_semicolon
       (fun (c,params,args) ->
 	hov 1 (str"(" ++ p_c c ++ str ")" ++ spc () ++ pr_sequence p_c params ++ spc () ++ str "(args:" ++
@@ -606,7 +606,7 @@ type local_state_reduction_function = evar_map -> state -> state
 
 let pr_state (tm,sk) =
   let open Pp in
-  let pr c = Termops.print_constr (EConstr.Unsafe.to_constr c) in
+  let pr c = Termops.print_constr c in
   h 0 (pr tm ++ str "|" ++ cut () ++ Stack.pr pr sk)
 
 let local_assum (na, t) =
@@ -835,7 +835,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
   let rec whrec cst_l (x, stack) =
     let () = if !debug_RAKAM then
 	let open Pp in
-	let pr c = Termops.print_constr (EConstr.Unsafe.to_constr c) in
+	let pr c = Termops.print_constr c in
 	Feedback.msg_notice
              (h 0 (str "<<" ++ pr x ++
 		   str "|" ++ cut () ++ Cst_stack.pr cst_l ++
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 233b58e91..c6fad1a34 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -671,16 +671,13 @@ let eta_constructor_app env sigma f l1 term =
       | _ -> assert false)
   | _ -> assert false
 
-let print_constr_env env c =
-  print_constr_env env (EConstr.Unsafe.to_constr c)
-
 let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top env cv_pb flags m n =
   let rec unirec_rec (curenv,nb as curenvnb) pb opt ((sigma,metasubst,evarsubst) as substn : subst0) curm curn =
     let cM = Evarutil.whd_head_evar sigma curm
     and cN = Evarutil.whd_head_evar sigma curn in
     let () = 
       if !debug_unification then
-	Feedback.msg_debug (print_constr_env curenv cM ++ str" ~= " ++ print_constr_env curenv cN)
+	Feedback.msg_debug (print_constr_env curenv sigma cM ++ str" ~= " ++ print_constr_env curenv sigma cN)
     in 
       match (EConstr.kind sigma cM, EConstr.kind sigma cN) with
 	| Meta k1, Meta k2 ->