Ltac now uses evar-based constrs.

4 files changed, 11 insertions, 10 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 393e958d38..7269c61e3d 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -575,10 +575,9 @@ let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma
 (* Pretty-print *)
 
 let pr_clenv clenv =
-  let inj = EConstr.Unsafe.to_constr in
   h 0
-    (str"TEMPL: " ++ print_constr (inj clenv.templval.rebus) ++
-     str" : " ++ print_constr (inj clenv.templtyp.rebus) ++ fnl () ++
+    (str"TEMPL: " ++ print_constr clenv.templval.rebus ++
+     str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++
      pr_evar_map (Some 2) clenv.evd)
 
 (****************************************************************)
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 8878051c89..0fe5c73f15 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -11,6 +11,7 @@ open CErrors
 open Util
 open Names
 open Term
+open EConstr
 open Declarations
 open Globnames
 open Genredexpr
@@ -200,9 +201,6 @@ let out_arg = function
 let out_with_occurrences (occs,c) =
   (Locusops.occurrences_map (List.map out_arg) occs, c)
 
-let out_with_occurrences' (occs,c) =
-  (Locusops.occurrences_map (List.map out_arg) occs, EConstr.of_constr c)
-
 let e_red f = { e_redfun = fun env evm c -> Sigma.here (f env (Sigma.to_evar_map evm) c) evm }
 
 let head_style = false (* Turn to true to have a semantics where simpl
@@ -242,8 +240,8 @@ let reduction_of_red_expr env =
      (e_red (strong_cbn (make_flag f)), DEFAULTcast)
   | Lazy f -> (e_red (clos_norm_flags (make_flag f)),DEFAULTcast)
   | Unfold ubinds -> (e_red (unfoldn (List.map out_with_occurrences ubinds)),DEFAULTcast)
-  | Fold cl -> (e_red (fold_commands (List.map EConstr.of_constr cl)),DEFAULTcast)
-  | Pattern lp -> (pattern_occs (List.map out_with_occurrences' lp),DEFAULTcast)
+  | Fold cl -> (e_red (fold_commands cl),DEFAULTcast)
+  | Pattern lp -> (pattern_occs (List.map out_with_occurrences lp),DEFAULTcast)
   | ExtraRedExpr s ->
       (try (e_red (String.Map.find s !reduction_tab),DEFAULTcast)
       with Not_found ->
@@ -256,9 +254,12 @@ let reduction_of_red_expr env =
   in
     reduction_of_red_expr
 
+let subst_mps subst c =
+  EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c))
+
 let subst_red_expr subs =
   Miscops.map_red_expr_gen
-    (Mod_subst.subst_mps subs)
+    (subst_mps subs)
     (Mod_subst.subst_evaluable_reference subs)
     (Patternops.subst_pattern subs)
 
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index d4c2c4a6c9..45e4610661 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -10,6 +10,7 @@
 
 open Names
 open Term
+open EConstr
 open Pattern
 open Genredexpr
 open Reductionops
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 7ffb30fa8d..3641ad74d7 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -144,7 +144,7 @@ open Pp
 let db_pr_goal sigma g =
   let env = Goal.V82.env sigma g in
   let penv = print_named_context env in
-  let pc = print_constr_env env (EConstr.Unsafe.to_constr (Goal.V82.concl sigma g)) in
+  let pc = print_constr_env env sigma (Goal.V82.concl sigma g) in
   str"  " ++ hv 0 (penv ++ fnl () ++
                    str "============================" ++ fnl ()  ++
                    str" "  ++ pc) ++ fnl ()