Proofview.Goal primitive now return EConstrs.

4 files changed, 10 insertions, 12 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 84cdc09ee..32c887ff5 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -144,7 +144,7 @@ let unify ?(flags=fail_quick_unif_flags) m =
     let n = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in
     let evd = clear_metas (Tacmach.New.project gl) in
     try
-      let evd' = w_unify env evd CONV ~flags m (EConstr.of_constr n) in
+      let evd' = w_unify env evd CONV ~flags m n in
 	Proofview.Unsafe.tclEVARSADVANCE evd'
     with e when CErrors.noncritical e -> Proofview.tclZERO e
   end }
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 11eabe0a9..32064aff5 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -77,7 +77,6 @@ let make_refine_enter ?(unsafe = true) f =
   let sigma = Sigma.to_evar_map sigma in
   let env = Proofview.Goal.env gl in
   let concl = Proofview.Goal.concl gl in
-  let concl = EConstr.of_constr concl in
   (** Save the [future_goals] state to restore them after the
       refinement. *)
   let prev_future_goals = Evd.future_goals sigma in
@@ -146,7 +145,6 @@ let with_type env evd c t =
 let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl ->
   let gl = Proofview.Goal.assume gl in
   let concl = Proofview.Goal.concl gl in
-  let concl = EConstr.of_constr concl in
   let env = Proofview.Goal.env gl in
   let f = { run = fun h ->
     let Sigma (c, h, p) = f.run h in
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index aa54e4f9b..f3f19e854 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -220,7 +220,7 @@ module New = struct
     let gl = Proofview.Goal.assume gl in
     let concl = Proofview.Goal.concl gl in
     let sigma = project gl in
-    nf_evar sigma concl
+    EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr concl))
 
   let pf_whd_all gl t = pf_apply whd_all gl t
 
@@ -229,13 +229,13 @@ module New = struct
   let pf_reduce_to_quantified_ind gl t =
     pf_apply reduce_to_quantified_ind gl t
 
-  let pf_hnf_constr gl t = pf_apply hnf_constr gl t
+  let pf_hnf_constr gl t = EConstr.of_constr (pf_apply hnf_constr gl t)
   let pf_hnf_type_of gl t =
-    pf_whd_all gl (EConstr.of_constr (pf_get_type_of gl t))
+    EConstr.of_constr (pf_whd_all gl (EConstr.of_constr (pf_get_type_of gl t)))
 
   let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t
 
-  let pf_whd_all gl t = pf_apply whd_all gl t
+  let pf_whd_all gl t = EConstr.of_constr (pf_apply whd_all gl t)
   let pf_compute gl t = pf_apply compute gl t
 
   let pf_nf_evar gl t = nf_evar (project gl) t
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 340c7addc..7b387ac9a 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -106,7 +106,7 @@ module New : sig
 
   val project : ('a, 'r) Proofview.Goal.t -> Evd.evar_map
   val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env
-  val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types
+  val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> EConstr.types
 
   val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> Term.types
   val pf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> evar_map * Term.types
@@ -120,13 +120,13 @@ module New : sig
   val pf_get_hyp_typ        : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> types
   val pf_last_hyp           : ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t
 
-  val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types
+  val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> EConstr.types
   val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> EConstr.types -> pinductive * EConstr.types
 
-  val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> types
-  val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> types
+  val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> EConstr.types
+  val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> EConstr.types
 
-  val pf_whd_all : ('a, 'r) Proofview.Goal.t -> EConstr.t -> constr
+  val pf_whd_all : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.constr
   val pf_compute : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.constr
 
   val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> EConstr.constr -> patvar_map