Reductionops now return EConstrs.

6 files changed, 22 insertions, 24 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 572db1d40..a428ab0ed 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -60,7 +60,7 @@ let refresh_undefined_univs clenv =
       { clenv with evd = evd'; templval = map_freelisted clenv.templval;
 	templtyp = map_freelisted clenv.templtyp }, subst
 
-let clenv_hnf_constr ce t = EConstr.of_constr (hnf_constr (cl_env ce) (cl_sigma ce) t)
+let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
 
 let clenv_get_type_of ce c = EConstr.of_constr (Retyping.get_type_of (cl_env ce) (cl_sigma ce) c)
 
@@ -71,7 +71,6 @@ let mk_freelisted c =
 
 let clenv_push_prod cl =
   let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in
-  let typ = EConstr.of_constr typ in
   let rec clrec typ = match EConstr.kind cl.evd typ with
     | Cast (t,_,_) -> clrec t
     | Prod (na,t,u) ->
@@ -266,7 +265,7 @@ let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv =
 
 let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl =
   let concl = Goal.V82.concl clenv.evd (sig_it gl) in
-  if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (EConstr.of_constr (whd_nored clenv.evd clenv.templtyp.rebus)))) then
+  if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd clenv.templtyp.rebus))) then
     clenv_unify CUMUL ~flags (clenv_type clenv) concl
       (clenv_unify_meta_types ~flags clenv)
   else
@@ -480,7 +479,7 @@ let error_already_defined b =
           (str "Position " ++ int n ++ str" already defined.")
 
 let clenv_unify_binding_type clenv c t u =
-  if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (EConstr.of_constr (whd_nored clenv.evd u)))) then
+  if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd u))) then
     (* Not enough information to know if some subtyping is needed *)
     CoerceToType, clenv, c
   else
@@ -498,7 +497,6 @@ let clenv_unify_binding_type clenv c t u =
 let clenv_assign_binding clenv k c =
   let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
   let c_typ = nf_betaiota clenv.evd (clenv_get_type_of clenv c) in
-  let c_typ = EConstr.of_constr c_typ in
   let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in
   let c = EConstr.Unsafe.to_constr c in
   { clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd }
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 829c96296..98ad9ebe3 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -34,7 +34,7 @@ type refiner_error =
   | CannotApply of constr * constr
   | NotWellTyped of constr
   | NonLinearProof of constr
-  | MetaInType of constr
+  | MetaInType of EConstr.constr
 
   (* Errors raised by the tactics *)
   | IntroNeedsProduct
@@ -347,10 +347,11 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
       match kind_of_term trm with
       | Meta _ ->
 	let conclty = nf_betaiota sigma (EConstr.of_constr conclty) in
-	  if !check && occur_meta sigma (EConstr.of_constr conclty) then
+	  if !check && occur_meta sigma conclty then
 	    raise (RefinerError (MetaInType conclty));
-	  let (gl,ev,sigma) = mk_goal hyps (EConstr.of_constr conclty) in
+	  let (gl,ev,sigma) = mk_goal hyps conclty in
 	  let ev = EConstr.Unsafe.to_constr ev in
+	  let conclty = EConstr.Unsafe.to_constr conclty in
 	  gl::goalacc, conclty, sigma, ev
 
       | Cast (t,k, ty) ->
@@ -425,7 +426,7 @@ and mk_hdgoals sigma goal goalacc trm =
   match kind_of_term trm with
     | Cast (c,_, ty) when isMeta c ->
 	check_typability env sigma ty;
-	let (gl,ev,sigma) = mk_goal hyps (EConstr.of_constr (nf_betaiota sigma (EConstr.of_constr ty))) in
+	let (gl,ev,sigma) = mk_goal hyps (nf_betaiota sigma (EConstr.of_constr ty)) in
 	let ev = EConstr.Unsafe.to_constr ev in
 	gl::goalacc,ty,sigma,ev
 
@@ -474,6 +475,7 @@ and mk_hdgoals sigma goal goalacc trm =
 and mk_arggoals sigma goal goalacc funty allargs =
   let foldmap (goalacc, funty, sigma) harg =
     let t = whd_all (Goal.V82.env sigma goal) sigma (EConstr.of_constr funty) in
+    let t = EConstr.Unsafe.to_constr t in
     let rec collapse t = match kind_of_term t with
     | LetIn (_, c1, _, b) -> collapse (subst1 c1 b)
     | _ -> t
@@ -537,7 +539,7 @@ let prim_refiner r sigma goal =
     (* Logical rules *)
     | Cut (b,replace,id,t) ->
 (*        if !check && not (Retyping.get_sort_of env sigma t) then*)
-        let (sg1,ev1,sigma) = mk_goal sign (EConstr.of_constr (nf_betaiota sigma (EConstr.of_constr t))) in
+        let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma (EConstr.of_constr t)) in
 	let sign,t,cl,sigma =
 	  if replace then
 	    let nexthyp = get_hyp_after id (named_context_of_val sign) in
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 8c8a01cad..5fe28ac76 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -43,7 +43,7 @@ type refiner_error =
   | CannotApply of constr * constr
   | NotWellTyped of constr
   | NonLinearProof of constr
-  | MetaInType of constr
+  | MetaInType of EConstr.constr
 
   (*i Errors raised by the tactics i*)
   | IntroNeedsProduct
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index d4a58da32..a830e25d9 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -44,7 +44,7 @@ let whd_cbn flags env sigma t =
   let (state,_) =
     (whd_state_gen true true flags env sigma (t,Reductionops.Stack.empty))
   in
-  EConstr.Unsafe.to_constr (Reductionops.Stack.zip ~refold:true sigma state)
+  Reductionops.Stack.zip ~refold:true sigma state
 
 let strong_cbn flags =
   strong (whd_cbn flags)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index f3f19e854..7ecf0a9e8 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -23,8 +23,6 @@ open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
 
-let compute env sigma c = EConstr.of_constr (compute env sigma c)
-
 let re_sig it  gc = { it = it; sigma = gc; }
 
 (**************************************************************)
@@ -229,13 +227,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 = EConstr.of_constr (pf_apply hnf_constr gl t)
+  let pf_hnf_constr gl t = pf_apply hnf_constr gl t
   let pf_hnf_type_of gl t =
-    EConstr.of_constr (pf_whd_all gl (EConstr.of_constr (pf_get_type_of gl t)))
+    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 = EConstr.of_constr (pf_apply whd_all gl t)
+  let pf_whd_all gl t = 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 7b387ac9a..21511b6f9 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -42,7 +42,7 @@ val pf_ids_of_hyps        : goal sigma -> Id.t list
 val pf_global             : goal sigma -> Id.t -> constr
 val pf_unsafe_type_of            : goal sigma -> EConstr.constr -> types
 val pf_type_of            : goal sigma -> EConstr.constr -> evar_map * types
-val pf_hnf_type_of        : goal sigma -> EConstr.constr -> types
+val pf_hnf_type_of        : goal sigma -> EConstr.constr -> EConstr.types
 
 val pf_get_hyp            : goal sigma -> Id.t -> Context.Named.Declaration.t
 val pf_get_hyp_typ        : goal sigma -> Id.t -> types
@@ -50,7 +50,7 @@ val pf_get_hyp_typ        : goal sigma -> Id.t -> types
 val pf_get_new_id  : Id.t      -> goal sigma -> Id.t
 val pf_get_new_ids : Id.t list -> goal sigma -> Id.t list
 
-val pf_reduction_of_red_expr : goal sigma -> red_expr -> EConstr.constr -> evar_map * constr
+val pf_reduction_of_red_expr : goal sigma -> red_expr -> EConstr.constr -> evar_map * EConstr.constr
 
 
 val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a
@@ -63,15 +63,15 @@ val pf_e_reduce :
   (env -> evar_map -> constr -> evar_map * constr) ->
   goal sigma -> constr -> evar_map * constr
 
-val pf_whd_all       : goal sigma -> EConstr.constr -> constr
-val pf_hnf_constr              : goal sigma -> EConstr.constr -> constr
-val pf_nf                      : goal sigma -> EConstr.constr -> constr
-val pf_nf_betaiota             : goal sigma -> EConstr.constr -> constr
+val pf_whd_all       : goal sigma -> EConstr.constr -> EConstr.constr
+val pf_hnf_constr              : goal sigma -> EConstr.constr -> EConstr.constr
+val pf_nf                      : goal sigma -> EConstr.constr -> EConstr.constr
+val pf_nf_betaiota             : goal sigma -> EConstr.constr -> EConstr.constr
 val pf_reduce_to_quantified_ind : goal sigma -> EConstr.types -> pinductive * EConstr.types
 val pf_reduce_to_atomic_ind     : goal sigma -> EConstr.types -> pinductive * EConstr.types
 val pf_compute                 : goal sigma -> EConstr.constr -> EConstr.constr
 val pf_unfoldn    : (occurrences * evaluable_global_reference) list
-  -> goal sigma -> EConstr.constr -> constr
+  -> goal sigma -> EConstr.constr -> EConstr.constr
 
 val pf_const_value : goal sigma -> pconstant -> constr
 val pf_conv_x      : goal sigma -> constr -> constr -> bool