Evar-normalizing functions now act on EConstrs.

11 files changed, 42 insertions, 46 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index eea94f021..0e4c6619b 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -362,7 +362,7 @@ let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) =
   let j = typing_fun tycon env evdref tomatch in
   let evd, j = Coercion.inh_coerce_to_base (loc_of_glob_constr tomatch) env !evdref j in
   evdref := evd;
-  let typ = EConstr.of_constr (nf_evar !evdref (EConstr.Unsafe.to_constr j.uj_type)) in
+  let typ = nf_evar !evdref j.uj_type in
   let t =
     try try_find_ind env !evdref typ realnames
     with Not_found ->
@@ -1145,7 +1145,7 @@ let postprocess_dependencies evd tocheck brs tomatch pred deps cs =
   let rec aux k brs tomatch pred tocheck deps = match deps, tomatch with
   | [], _ -> brs,tomatch,pred,[]
   | n::deps, Abstract (i,d) :: tomatch ->
-      let d = map_constr (nf_evar evd) d in
+      let d = map_constr (fun c -> EConstr.Unsafe.to_constr (nf_evar evd (EConstr.of_constr c))) d in
       let is_d = match d with LocalAssum _ -> false | LocalDef _ -> true in
       if is_d || List.exists (fun c -> dependent_decl evd (lift k c) d) tocheck
                  && Array.exists (is_dependent_branch evd k) brs then
@@ -2008,9 +2008,9 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
       let envar = List.fold_right push_rel_context arsign env in
       let sigma, newt = new_sort_variable univ_flexible_alg sigma in
       let evdref = ref sigma in
-      let predcclj = typing_fun (mk_tycon (EConstr.mkSort newt)) envar evdref rtntyp in
+      let predcclj = typing_fun (mk_tycon (mkSort newt)) envar evdref rtntyp in
       let sigma = !evdref in
-      let predccl = EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr predcclj.uj_val)) in
+      let predccl = nf_evar sigma predcclj.uj_val in
       [sigma, predccl]
   in
   List.map
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index ead44cee2..91f53a886 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -417,7 +417,6 @@ let inh_tosort_force loc env evd j =
   try
     let t,p = lookup_path_to_sort_from env evd j.uj_type in
     let evd,j1 = apply_coercion env evd p j t in
-    let whd_evar evd c = EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr c)) in
     let j2 = on_judgment_type (whd_evar evd) j1 in
       (evd,type_judgment env evd j2)
   with Not_found | NoCoercion ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 87267d538..3ae2e35e6 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -526,7 +526,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	  | None, Success i' ->
             (* We do have sk1[] = sk2[]: we now unify ?ev1 and ?ev2 *)
             (* Note that ?ev1 and ?ev2, may have been instantiated in the meantime *)
-	    let ev1' = EConstr.of_constr (whd_evar i' (EConstr.Unsafe.to_constr (mkEvar ev1))) in
+	    let ev1' = whd_evar i' (mkEvar ev1) in
 	      if isEvar i' ev1' then
 		solve_simple_eqn (evar_conv_x ts) env i'
 		  (position_problem true pbty,destEvar i' ev1', term2)
@@ -536,7 +536,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	  | Some (r,[]), Success i' ->
             (* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *)
             (* we now unify r[?ev1] and ?ev2 *)
-	    let ev2' = EConstr.of_constr (whd_evar i' (EConstr.Unsafe.to_constr (mkEvar ev2))) in
+	    let ev2' = whd_evar i' (mkEvar ev2) in
 	      if isEvar i' ev2' then
 		solve_simple_eqn (evar_conv_x ts) env i'
 		  (position_problem false pbty,destEvar i' ev2',Stack.zip evd (term1,r))
@@ -547,7 +547,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
             (* Symmetrically *)
             (* We have sk1[] = sk2'[] for some sk2' s.t. sk2[]=sk2'[r[]] *)
             (* we now unify ?ev1 and r[?ev2] *)
-	    let ev1' = EConstr.of_constr (whd_evar i' (EConstr.Unsafe.to_constr (mkEvar ev1))) in
+	    let ev1' = whd_evar i' (mkEvar ev1) in
 	      if isEvar i' ev1' then
 		solve_simple_eqn (evar_conv_x ts) env i'
 	          (position_problem true pbty,destEvar i' ev1',Stack.zip evd (term2,r))
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index 875e4a118..5831d3191 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -33,8 +33,9 @@ let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal t
   (Sigma.to_evar_map evd, evk)
 
 let env_nf_evar sigma env =
+  let nf_evar c = EConstr.Unsafe.to_constr (nf_evar sigma (EConstr.of_constr c)) in
   process_rel_context
-    (fun d e -> push_rel (RelDecl.map_constr (nf_evar sigma) d) e) env
+    (fun d e -> push_rel (RelDecl.map_constr nf_evar d) e) env
 
 let env_nf_betaiotaevar sigma env =
   process_rel_context
@@ -144,7 +145,7 @@ let define_pure_evar_as_lambda env evd evk =
   | _ -> error_not_product env evd typ in
   let avoid = ids_of_named_context (evar_context evi) in
   let id =
-    next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd (EConstr.Unsafe.to_constr dom)) in
+    next_name_away_with_default_using_types "x" na avoid (EConstr.Unsafe.to_constr (Reductionops.whd_evar evd dom)) in
   let newenv = push_named (nlocal_assum (id, dom)) evenv in
   let filter = Filter.extend 1 (evar_filter evi) in
   let src = evar_source evk evd1 in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index de2e46a78..3235c2505 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -601,13 +601,13 @@ let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_si
   let evd = Sigma.Unsafe.of_evar_map evd in
   let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in
   let evd = Sigma.to_evar_map evd in
-  let t_in_env = EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr t_in_env)) in
+  let t_in_env = whd_evar evd t_in_env in
   let (evk, _) = destEvar evd evar_in_env in
   let evd = define_fun env evd None (destEvar evd evar_in_env) t_in_env in
   let ctxt = named_context_of_val sign in
   let inst_in_sign = inst_of_vars (Filter.filter_list filter ctxt) in
   let evar_in_sign = mkEvar (evk, inst_in_sign) in
-  (evd,EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr evar_in_sign)))
+  (evd,whd_evar evd evar_in_sign)
 
 (* We have x1..xq |- ?e1 : τ and had to solve something like
  * Σ; Γ |- ?e1[u1..uq] = (...\y1 ... \yk ... c), where c is typically some
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 673554005..24f6d1689 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -10,50 +10,51 @@ open Util
 open Names
 open Term
 open Environ
+open EConstr
 open Type_errors
 
 type unification_error =
-  | OccurCheck of existential_key * EConstr.constr
-  | NotClean of EConstr.existential * env * EConstr.constr (* Constr is a variable not in scope *)
+  | OccurCheck of existential_key * constr
+  | NotClean of existential * env * constr (* Constr is a variable not in scope *)
   | NotSameArgSize
   | NotSameHead
   | NoCanonicalStructure
-  | ConversionFailed of env * EConstr.constr * EConstr.constr (* Non convertible closed terms *)
+  | ConversionFailed of env * constr * constr (* Non convertible closed terms *)
   | MetaOccurInBody of existential_key
-  | InstanceNotSameType of existential_key * env * EConstr.types * EConstr.types
+  | InstanceNotSameType of existential_key * env * types * types
   | UnifUnivInconsistency of Univ.univ_inconsistency
   | CannotSolveConstraint of Evd.evar_constraint * unification_error
   | ProblemBeyondCapabilities
 
 type position = (Id.t * Locus.hyp_location_flag) option
 
-type position_reporting = (position * int) * EConstr.t
+type position_reporting = (position * int) * constr
 
-type subterm_unification_error = bool * position_reporting * position_reporting * (EConstr.constr * EConstr.constr * unification_error) option
+type subterm_unification_error = bool * position_reporting * position_reporting * (constr * constr * unification_error) option
 
-type type_error = (EConstr.constr, EConstr.types) ptype_error
+type type_error = (constr, types) ptype_error
 
 type pretype_error =
   (* Old Case *)
-  | CantFindCaseType of EConstr.constr
+  | CantFindCaseType of constr
   (* Type inference unification *)
-  | ActualTypeNotCoercible of EConstr.unsafe_judgment * EConstr.types * unification_error
+  | ActualTypeNotCoercible of unsafe_judgment * types * unification_error
   (* Tactic unification *)
-  | UnifOccurCheck of existential_key * EConstr.constr
+  | UnifOccurCheck of existential_key * constr
   | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option
-  | CannotUnify of EConstr.constr * EConstr.constr * unification_error option
-  | CannotUnifyLocal of EConstr.constr * EConstr.constr * EConstr.constr
+  | CannotUnify of constr * constr * unification_error option
+  | CannotUnifyLocal of constr * constr * constr
   | CannotUnifyBindingType of constr * constr
   | CannotGeneralize of constr
-  | NoOccurrenceFound of EConstr.constr * Id.t option
-  | CannotFindWellTypedAbstraction of EConstr.constr * EConstr.constr list * (env * type_error) option
-  | WrongAbstractionType of Name.t * EConstr.constr * EConstr.types * EConstr.types
+  | NoOccurrenceFound of constr * Id.t option
+  | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option
+  | WrongAbstractionType of Name.t * constr * types * types
   | AbstractionOverMeta of Name.t * Name.t
-  | NonLinearUnification of Name.t * EConstr.constr
+  | NonLinearUnification of Name.t * constr
   (* Pretyping *)
   | VarNotFound of Id.t
-  | UnexpectedType of EConstr.constr * EConstr.constr
-  | NotProduct of EConstr.constr
+  | UnexpectedType of constr * constr
+  | NotProduct of constr
   | TypingError of type_error
   | CannotUnifyOccurrences of subterm_unification_error
   | UnsatisfiableConstraints of
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 7cef14339..c303d5d94 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -45,8 +45,8 @@ type pretype_error =
   | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option
   | CannotUnify of constr * constr * unification_error option
   | CannotUnifyLocal of constr * constr * constr
-  | CannotUnifyBindingType of Constr.constr * Constr.constr
-  | CannotGeneralize of Constr.constr
+  | CannotUnifyBindingType of constr * constr
+  | CannotGeneralize of constr
   | NoOccurrenceFound of constr * Id.t option
   | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option
   | WrongAbstractionType of Name.t * constr * types * types
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 6b6800ac6..4660978df 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -143,9 +143,6 @@ let nf_fix sigma (nas, cs, ts) =
   let inj c = EConstr.to_constr sigma c in
   (nas, Array.map inj cs, Array.map inj ts)
 
-let nf_evar sigma c =
-  EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr c))
-
 let search_guard loc env possible_indexes fixdefs =
   (* Standard situation with only one possibility for each fix. *)
   (* We treat it separately in order to get proper error msg. *)
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 8aaeeb2c2..dcc11cfcf 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -156,11 +156,11 @@ val nf_beta : local_reduction_function
 val nf_betaiota : local_reduction_function
 val nf_betaiotazeta : local_reduction_function
 val nf_all : reduction_function
-val nf_evar : evar_map -> Constr.constr -> Constr.constr
+val nf_evar : evar_map -> constr -> constr
 
 (** Lazy strategy, weak head reduction *)
 
-val whd_evar :  evar_map -> Constr.constr -> Constr.constr
+val whd_evar :  evar_map -> constr -> constr
 val whd_nored : local_reduction_function
 val whd_beta : local_reduction_function
 val whd_betaiota : local_reduction_function
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 7baff421f..e6f1e46b6 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -252,7 +252,7 @@ let judge_of_letin env name defj typj j =
 (* cstr must be in n.f. w.r.t. evars and execute returns a judgement
    where both the term and type are in n.f. *)
 let rec execute env evdref cstr =
-  let cstr = EConstr.of_constr (whd_evar !evdref (EConstr.Unsafe.to_constr cstr)) in
+  let cstr = whd_evar !evdref cstr in
   match EConstr.kind !evdref cstr with
     | Meta n ->
         { uj_val = cstr; uj_type = meta_type !evdref n }
@@ -411,6 +411,6 @@ let e_solve_evars env evdref c =
   let env = enrich_env env evdref in
   let c = (execute env evdref c).uj_val in
   (* side-effect on evdref *)
-  EConstr.of_constr (nf_evar !evdref (EConstr.Unsafe.to_constr c))
+  nf_evar !evdref c
 
 let _ = Evarconv.set_solve_evars (fun env evdref c -> e_solve_evars env evdref c)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 20f27a15a..1dc3ccdc0 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -137,7 +137,7 @@ let abstract_list_all_with_dependencies env evd typ c l =
     Evarconv.second_order_matching empty_transparent_state
       env evd ev' argoccs c in
   if b then
-    let p = nf_evar evd (EConstr.Unsafe.to_constr ev) in
+    let p = nf_evar evd ev in
       evd, p
   else error_cannot_find_well_typed_abstraction env evd 
     c l None
@@ -1240,7 +1240,7 @@ let try_to_coerce env evd c cty tycon =
   let j = make_judge c cty in
   let (evd',j') = inh_conv_coerce_rigid_to true Loc.ghost env evd j tycon in
   let evd' = Evarconv.consider_remaining_unif_problems env evd' in
-  let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in
+  let evd' = Evd.map_metas_fvalue (fun c -> EConstr.Unsafe.to_constr (nf_evar evd' (EConstr.of_constr c))) evd' in
     (evd',j'.uj_val)
 
 let w_coerce_to_type env evd c cty mvty =
@@ -1397,7 +1397,7 @@ let w_merge env with_types flags (evd,metas,evars : subst0) =
     let evd''' = w_merge_rec evd'' mc ec [] in
     if evd' == evd'''
     then Evd.define sp (EConstr.Unsafe.to_constr c) evd'''
-    else Evd.define sp (Evarutil.nf_evar evd''' (EConstr.Unsafe.to_constr c)) evd''' in
+    else Evd.define sp (EConstr.Unsafe.to_constr (Evarutil.nf_evar evd''' c)) evd''' in
 
   let check_types evd = 
     let metas = Evd.meta_list evd in
@@ -1513,8 +1513,7 @@ let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sig
   let current_sigma = Sigma.to_evar_map current_sigma in
   let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in
   let sigma, subst = nf_univ_variables sigma in
-  let c = EConstr.Unsafe.to_constr c in
-  Sigma.Unsafe.of_pair (EConstr.of_constr (CVars.subst_univs_constr subst (nf_evar sigma c)), sigma)
+  Sigma.Unsafe.of_pair (EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c))), sigma)
 
 let default_matching_core_flags sigma =
   let ts = Names.full_transparent_state in {
@@ -1602,7 +1601,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
   (fun test -> match test.testing_state with
   | None -> None
   | Some (sigma,_,l) ->
-     let c = applist (EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr (local_strong whd_meta sigma c))), l) in
+     let c = applist (nf_evar sigma (local_strong whd_meta sigma c), l) in
      let univs, subst = nf_univ_variables sigma in
      Some (sigma,EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr c))))
 
@@ -1926,7 +1925,6 @@ let secondOrderAbstraction env evd flags typ (p, oplist) =
 let secondOrderDependentAbstraction env evd flags typ (p, oplist) =
   let typp = Typing.meta_type evd p in
   let evd, pred = abstract_list_all_with_dependencies env evd typp typ oplist in
-  let pred = EConstr.of_constr pred in
   w_merge env false flags.merge_unify_flags
     (evd,[p,pred,(Conv,TypeProcessed)],[])