Evar maps contain econstrs.

We bootstrap the circular evar_map <-> econstr dependency by moving
the internal EConstr.API module to Evd.MiniEConstr. Then we make the
Evd functions use econstr.

15 files changed, 78 insertions, 109 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index b16f1a9ed..4c87b4e7e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1015,7 +1015,7 @@ let adjust_impossible_cases pb pred tomatch submat =
     | Evar (evk,_) when snd (evar_source evk !(pb.evdref)) == Evar_kinds.ImpossibleCase ->
         if not (Evd.is_defined !(pb.evdref) evk) then begin
 	  let evd, default = use_unit_judge !(pb.evdref) in
-	  pb.evdref := Evd.define evk (EConstr.Unsafe.to_constr default.uj_type) evd
+          pb.evdref := Evd.define evk default.uj_type evd
         end;
         add_assert_false_case pb tomatch
     | _ ->
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 04cb6a59f..6dc3687a0 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -251,7 +251,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
 			     let (n, dom, rng) = destLambda !evdref t in
 			       if isEvar !evdref dom then
 				 let (domk, args) = destEvar !evdref dom in
-				   evdref := define domk (EConstr.Unsafe.to_constr a) !evdref;
+                                   evdref := define domk a !evdref;
 			       else ();
 			       t, rng
 		       | _ -> raise NoSubtacCoercion
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index d37090a65..144166a34 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -114,9 +114,6 @@ let flex_kind_of_term ts env evd c sk =
     | Fix _ -> Rigid (* happens when the fixpoint is partially applied *)
     | Cast _ | App _ | Case _ -> assert false
 
-let add_conv_pb (pb, env, x, y) sigma =
-  Evd.add_conv_pb (pb, env, EConstr.Unsafe.to_constr x, EConstr.Unsafe.to_constr y) sigma
-
 let apprec_nohdbeta ts env evd c =
   let (t,sk as appr) = Reductionops.whd_nored_state evd (c, []) in
   if Stack.not_purely_applicative sk
@@ -1045,7 +1042,7 @@ let choose_less_dependent_instance evk evd term args =
   let subst' = List.filter (fun (id,c) -> EConstr.eq_constr evd c term) subst in
   match subst' with
   | [] -> None
-  | (id, _) :: _ -> Some (Evd.define evk (Constr.mkVar id) evd)
+  | (id, _) :: _ -> Some (Evd.define evk (mkVar id) evd)
 
 let apply_on_subterm env evdref f c t =
   let rec applyrec (env,(k,c) as acc) t =
@@ -1085,7 +1082,7 @@ let filter_possible_projections evd c ty ctxt args =
     let a = Array.unsafe_get args i in
     (match decl with
      | NamedDecl.LocalAssum _ -> false
-     | NamedDecl.LocalDef (_,c,_) -> not (isRel evd (EConstr.of_constr c) || isVar evd (EConstr.of_constr c))) ||
+     | NamedDecl.LocalDef (_,c,_) -> not (isRel evd c || isVar evd c)) ||
     a == c ||
     (* Here we make an approximation, for instance, we could also be *)
     (* interested in finding a term u convertible to c such that a occurs *)
@@ -1135,7 +1132,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
       end
   | decl'::ctxt', c::l, occs::occsl ->
       let id = NamedDecl.get_id decl' in
-      let t = EConstr.of_constr (NamedDecl.get_type decl') in
+      let t = NamedDecl.get_type decl' in
       let evs = ref [] in
       let ty = Retyping.get_type_of env_rhs evd c in
       let filter' = filter_possible_projections evd c ty ctxt args in
@@ -1183,7 +1180,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
               (* We force abstraction over this unconstrained occurrence *)
               (* and we use typing to propagate this instantiation *)
               (* This is an arbitrary choice *)
-              let evd = Evd.define evk (Constr.mkVar id) evd in
+              let evd = Evd.define evk (mkVar id) evd in
               match evar_conv_x ts env_evar evd CUMUL idty evty with
               | UnifFailure _ -> user_err Pp.(str "Cannot find an instance")
               | Success evd ->
@@ -1205,14 +1202,11 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
 	    (evar_conv_x full_transparent_state)
       with IllTypedInstance _ -> raise (TypingFailed evd)
     in
-      Evd.define evk (EConstr.Unsafe.to_constr rhs) evd 
+      Evd.define evk rhs evd
   in
   abstract_free_holes evd subst, true
   with TypingFailed evd -> evd, false
 
-let to_pb (pb, env, t1, t2) =
-  (pb, env, EConstr.Unsafe.to_constr t1, EConstr.Unsafe.to_constr t2)
-
 let second_order_matching_with_args ts env evd pbty ev l t =
 (*
   let evd,ev = evar_absorb_arguments env evd ev l in
@@ -1222,7 +1216,7 @@ let second_order_matching_with_args ts env evd pbty ev l t =
   else UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t))
   if b then Success evd else
  *)
-  let pb = to_pb (pbty,env,mkApp(mkEvar ev,l),t) in
+  let pb = (pbty,env,mkApp(mkEvar ev,l),t) in
   UnifFailure (evd, CannotSolveConstraint (pb,ProblemBeyondCapabilities))
 
 let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
@@ -1245,7 +1239,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
       | Some evd -> Success evd
       | None ->
          let reason = ProblemBeyondCapabilities in
-         UnifFailure (evd, CannotSolveConstraint (to_pb (pbty,env,t1,t2),reason)))
+         UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason)))
   | (Rel _|Var _), Evar (evk2,args2) when app_empty
       && List.for_all (fun a -> EConstr.eq_constr evd a term1 || isEvar evd a)
         (remove_instance_local_defs evd evk2 args2) ->
@@ -1255,7 +1249,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
       | Some evd -> Success evd
       | None ->
          let reason = ProblemBeyondCapabilities in
-         UnifFailure (evd, CannotSolveConstraint (to_pb (pbty,env,t1,t2),reason)))
+         UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason)))
   | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 ->
       let f env evd pbty x y = is_fconv ~reds:ts pbty env evd x y in
       Success (solve_refl ~can_drop:true f env evd
@@ -1295,10 +1289,10 @@ let error_cannot_unify env evd pb ?reason t1 t2 =
 
 let check_problems_are_solved env evd =
   match snd (extract_all_conv_pbs evd) with
-  | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb (EConstr.of_constr t1) (EConstr.of_constr t2)
+  | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb t1 t2
   | _ -> ()
 
-exception MaxUndefined of (Evar.t * evar_info * Constr.t list)
+exception MaxUndefined of (Evar.t * evar_info * EConstr.t list)
 
 let max_undefined_with_candidates evd =
   let fold evk evi () = match evi.evar_candidates with
@@ -1326,7 +1320,7 @@ let rec solve_unconstrained_evars_with_candidates ts evd =
       | a::l ->
           try
             let conv_algo = evar_conv_x ts in
-            let evd = check_evar_instance evd evk (EConstr.of_constr a) conv_algo in
+            let evd = check_evar_instance evd evk a conv_algo in
             let evd = Evd.define evk a evd in
             match reconsider_unif_constraints conv_algo evd with
             | Success evd -> solve_unconstrained_evars_with_candidates ts evd
@@ -1348,7 +1342,7 @@ let solve_unconstrained_impossible_cases env evd =
       let ty = j_type j in
       let conv_algo = evar_conv_x full_transparent_state in
       let evd' = check_evar_instance evd' evk ty conv_algo in
-	Evd.define evk (EConstr.Unsafe.to_constr ty) evd' 
+        Evd.define evk ty evd'
     | _ -> evd') evd evd
 
 let solve_unif_constraints_with_heuristics env
@@ -1357,8 +1351,6 @@ let solve_unif_constraints_with_heuristics env
   let rec aux evd pbs progress stuck =
     match pbs with
     | (pbty,env,t1,t2 as pb) :: pbs ->
-        let t1 = EConstr.of_constr t1 in
-        let t2 = EConstr.of_constr t2 in
         (match apply_conversion_problem_heuristic ts env evd pbty t1 t2 with
 	| Success evd' ->
 	    let (evd', rest) = extract_all_conv_pbs evd' in
@@ -1375,9 +1367,7 @@ let solve_unif_constraints_with_heuristics env
 	  match stuck with
 	  | [] -> (* We're finished *) evd
 	  | (pbty,env,t1,t2 as pb) :: _ ->
-            let t1 = EConstr.of_constr t1 in
-            let t2 = EConstr.of_constr t2 in
-	     (* There remains stuck problems *)
+             (* There remains stuck problems *)
              error_cannot_unify env evd pb t1 t2
   in
   let (evd,pbs) = extract_all_conv_pbs evd in
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index 4cffbbb83..b452755b1 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -77,7 +77,7 @@ let define_pure_evar_as_product evd evk =
   let evi = Evd.find_undefined evd evk in
   let evenv = evar_env evi in
   let id = next_ident_away idx (Environ.ids_of_named_context_val evi.evar_hyps) in
-  let concl = Reductionops.whd_all evenv evd (EConstr.of_constr evi.evar_concl) in
+  let concl = Reductionops.whd_all evenv evd evi.evar_concl in
   let s = destSort evd concl in
   let evksrc = evar_source evk evd in
   let src = subterm_source evk ~where:Domain evksrc in
@@ -101,7 +101,7 @@ let define_pure_evar_as_product evd evk =
 	  evd3, rng
   in
   let prod = mkProd (Name id, dom, subst_var id rng) in
-  let evd3 = Evd.define evk (EConstr.Unsafe.to_constr prod) evd2 in
+  let evd3 = Evd.define evk prod evd2 in
     evd3,prod
 
 (* Refine an applied evar to a product and returns its instantiation *)
@@ -128,7 +128,7 @@ let define_pure_evar_as_lambda env evd evk =
   let open Context.Named.Declaration in
   let evi = Evd.find_undefined evd evk in
   let evenv = evar_env evi in
-  let typ = Reductionops.whd_all evenv evd (EConstr.of_constr (evar_concl evi)) in
+  let typ = Reductionops.whd_all evenv evd (evar_concl evi) in
   let evd1,(na,dom,rng) = match EConstr.kind evd typ with
   | Prod (na,dom,rng) -> (evd,(na,dom,rng))
   | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd evd typ
@@ -141,7 +141,7 @@ let define_pure_evar_as_lambda env evd evk =
   let src = subterm_source evk ~where:Body (evar_source evk evd1) in
   let evd2,body = new_evar newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in
   let lam = mkLambda (Name id, dom, subst_var id body) in
-  Evd.define evk (EConstr.Unsafe.to_constr lam) evd2, lam
+  Evd.define evk lam evd2, lam
 
 let define_evar_as_lambda env evd (evk,args) =
   let evd,lam = define_pure_evar_as_lambda env evd evk in
@@ -166,9 +166,9 @@ let define_evar_as_sort env evd (ev,args) =
   let evd, u = new_univ_variable univ_rigid evd in
   let evi = Evd.find_undefined evd ev in 
   let s = Type u in
-  let concl = Reductionops.whd_all (evar_env evi) evd (EConstr.of_constr evi.evar_concl) in
+  let concl = Reductionops.whd_all (evar_env evi) evd evi.evar_concl in
   let sort = destSort evd concl in
-  let evd' = Evd.define ev (Constr.mkSort s) evd in
+  let evd' = Evd.define ev (mkSort s) evd in
   Evd.set_leq_sort env evd' (Type (Univ.super u)) (ESorts.kind evd' sort), s
 
 (* Propagation of constraints through application and abstraction:
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 0c109b026..b7eaff078 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -89,9 +89,9 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
       Array.iter (refresh_term_evars onevars false) args
     | Evar (ev, a) when onevars ->
       let evi = Evd.find !evdref ev in
-      let ty' = refresh ~onlyalg univ_flexible ~direction:true (EConstr.of_constr evi.evar_concl) in
+      let ty' = refresh ~onlyalg univ_flexible ~direction:true evi.evar_concl in
 	if !modified then 
-	  evdref := Evd.add !evdref ev {evi with evar_concl = EConstr.Unsafe.to_constr ty'}
+          evdref := Evd.add !evdref ev {evi with evar_concl = ty'}
 	else ()
     | _ -> EConstr.iter !evdref (refresh_term_evars onevars false) t
   and refresh_polymorphic_positions args pos =
@@ -137,8 +137,6 @@ let test_success conv_algo env evd c c' rhs =
   is_success (conv_algo env evd c c' rhs)
 
 let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd =
-  let t1 = EConstr.Unsafe.to_constr t1 in
-  let t2 = EConstr.Unsafe.to_constr t2 in
   match pbty with
   | Some true -> add_conv_pb ~tail (Reduction.CUMUL,env,t1,t2) evd
   | Some false -> add_conv_pb ~tail (Reduction.CUMUL,env,t2,t1) evd
@@ -197,7 +195,7 @@ let restrict_evar_key evd evk filter candidates =
       | None -> evar_filter evi
       | Some filter -> filter in
       let candidates = match candidates with
-      | NoUpdate -> Option.map (fun l -> List.map EConstr.of_constr l) evi.evar_candidates
+      | NoUpdate -> evi.evar_candidates
       | UpdateWith c -> Some c in
       restrict_evar evd evk filter candidates
     end
@@ -600,7 +598,6 @@ let solve_pattern_eqn env sigma l c =
 
 let make_projectable_subst aliases sigma evi args =
   let sign = evar_filtered_context evi in
-  let sign = List.map (fun d -> map_named_decl EConstr.of_constr d) sign in
   let evar_aliases = compute_var_aliases sign sigma in
   let (_,full_subst,cstr_subst) =
     List.fold_right
@@ -877,7 +874,7 @@ let choose_projection evi sols =
 let rec do_projection_effects define_fun env ty evd = function
   | ProjectVar -> evd
   | ProjectEvar ((evk,argsv),evi,id,p) ->
-      let evd = Evd.define evk (Constr.mkVar id) evd in
+      let evd = Evd.define evk (mkVar id) evd in
       (* TODO: simplify constraints involving evk *)
       let evd = do_projection_effects define_fun env ty evd p in
       let ty = whd_all env evd (Lazy.force ty) in
@@ -887,7 +884,7 @@ let rec do_projection_effects define_fun env ty evd = function
            one (however, regarding coercions, because t is obtained by
            unif, we know that no coercion can be inserted) *)
         let subst = make_pure_subst evi argsv in
-        let ty' = replace_vars subst (EConstr.of_constr evi.evar_concl) in
+        let ty' = replace_vars subst evi.evar_concl in
         if isEvar evd ty' then define_fun env evd (Some false) (destEvar evd ty') ty else evd
       else
         evd
@@ -1004,7 +1001,7 @@ let filter_effective_candidates evd evi filter candidates =
 let filter_candidates evd evk filter candidates_update =
   let evi = Evd.find_undefined evd evk in
   let candidates = match candidates_update with
-  | NoUpdate -> Option.map (fun l -> List.map EConstr.of_constr l) evi.evar_candidates
+  | NoUpdate -> evi.evar_candidates
   | UpdateWith c -> Some c
   in
   match candidates with
@@ -1023,13 +1020,12 @@ let closure_of_filter evd evk = function
   | None -> None
   | Some filter ->
   let evi = Evd.find_undefined evd evk in
-  let vars = collect_vars evd (EConstr.of_constr (evar_concl evi)) in
+  let vars = collect_vars evd (evar_concl evi) in
   let test b decl = b || Id.Set.mem (get_id decl) vars ||
                     match decl with
                     | LocalAssum _ ->
                        false
                     | LocalDef (_,c,_) ->
-                      let c = EConstr.of_constr c in
                        not (isRel evd c || isVar evd c)
   in
   let newfilter = Filter.map_along test filter (evar_context evi) in
@@ -1062,7 +1058,7 @@ let do_restrict_hyps evd (evk,args as ev) filter candidates =
   match candidates,filter with
   | UpdateWith [], _ -> user_err Pp.(str "Not solvable.")
   | UpdateWith [nc],_ ->
-      let evd = Evd.define evk (EConstr.Unsafe.to_constr nc) evd in
+      let evd = Evd.define evk nc evd in
       raise (EvarSolvedWhileRestricting (evd,mkEvar ev))
   | NoUpdate, None -> evd,ev
   | _ -> restrict_applied_evar evd ev filter candidates
@@ -1113,9 +1109,6 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs =
  * Note: argument f is the function used to instantiate evars.
  *)
 
-let instantiate_evar_array evi c args =
-  EConstr.of_constr (instantiate_evar_array evi (EConstr.Unsafe.to_constr c) (Array.map EConstr.Unsafe.to_constr args))
-
 let filter_compatible_candidates conv_algo env evd evi args rhs c =
   let c' = instantiate_evar_array evi c args in
   match conv_algo env evd Reduction.CONV rhs c' with
@@ -1135,8 +1128,6 @@ let restrict_candidates conv_algo env evd filter1 (evk1,argsv1) (evk2,argsv2) =
   | _, None -> filter_candidates evd evk1 filter1 NoUpdate
   | None, Some _ -> raise DoesNotPreserveCandidateRestriction
   | Some l1, Some l2 ->
-      let l1 = List.map EConstr.of_constr l1 in
-      let l2 = List.map EConstr.of_constr l2 in
       let l1 = filter_effective_candidates evd evi1 filter1 l1 in
       let l1' = List.filter (fun c1 ->
         let c1' = instantiate_evar_array evi1 c1 argsv1 in
@@ -1242,9 +1233,9 @@ let check_evar_instance evd evk1 body conv_algo =
     try Retyping.get_type_of ~lax:true evenv evd body
     with Retyping.RetypeError _ -> user_err Pp.(str "Ill-typed evar instance")
   in
-  match conv_algo evenv evd Reduction.CUMUL ty (EConstr.of_constr evi.evar_concl) with
+  match conv_algo evenv evd Reduction.CUMUL ty evi.evar_concl with
   | Success evd -> evd
-  | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,EConstr.of_constr evi.evar_concl))
+  | UnifFailure _ -> raise (IllTypedInstance (evenv,ty, evi.evar_concl))
 
 let update_evar_source ev1 ev2 evd =
   let loc, evs2 = evar_source ev2 evd in
@@ -1257,7 +1248,7 @@ let update_evar_source ev1 ev2 evd =
 let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) =
   try
     let evd,body = project_evar_on_evar force g env evd aliases 0 pbty ev1 ev2 in
-    let evd' = Evd.define evk2 (EConstr.Unsafe.to_constr body) evd in
+    let evd' = Evd.define evk2 body evd in
     let evd' = update_evar_source (fst (destEvar evd body)) evk2 evd' in
       check_evar_instance evd' evk2 body g
   with EvarSolvedOnTheFly (evd,c) ->
@@ -1292,17 +1283,19 @@ let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 a
 let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
   let pbty = if force then None else pbty in
   let evi = Evd.find evd evk1 in
-  let downcast evk t evd = downcast evk (EConstr.Unsafe.to_constr t) evd in
+  let downcast evk t evd = downcast evk t evd in
   let evd =
     try 
       (* ?X : Π Δ. Type i = ?Y : Π Δ'. Type j.
 	 The body of ?X and ?Y just has to be of type Π Δ. Type k for some k <= i, j. *)
       let evienv = Evd.evar_env evi in
-      let ctx1, i = Reduction.dest_arity evienv evi.evar_concl in
+      let concl1 = EConstr.Unsafe.to_constr evi.evar_concl in
+      let ctx1, i = Reduction.dest_arity evienv concl1 in
       let ctx1 = List.map (fun c -> map_rel_decl EConstr.of_constr c) ctx1 in
       let evi2 = Evd.find evd evk2 in
       let evi2env = Evd.evar_env evi2 in
-      let ctx2, j = Reduction.dest_arity evi2env evi2.evar_concl in
+      let concl2 = EConstr.Unsafe.to_constr evi2.evar_concl in
+      let ctx2, j = Reduction.dest_arity evi2env concl2 in
       let ctx2 = List.map (fun c -> map_rel_decl EConstr.of_constr c) ctx2 in
       let ui, uj = univ_of_sort i, univ_of_sort j in
 	if i == j || Evd.check_eq evd ui uj
@@ -1375,14 +1368,14 @@ let solve_candidates conv_algo env evd (evk,argsv) rhs =
   | Some l ->
       let l' =
         List.map_filter
-          (fun c -> filter_compatible_candidates conv_algo env evd evi argsv rhs (EConstr.of_constr c)) l in
+          (fun c -> filter_compatible_candidates conv_algo env evd evi argsv rhs c) l in
       match l' with
       | [] -> raise IncompatibleCandidates
       | [c,evd] ->
           (* solve_candidates might have been called recursively in the mean *)
           (* time and the evar been solved by the filtering process *)
          if Evd.is_undefined evd evk then
-	   let evd' = Evd.define evk (EConstr.Unsafe.to_constr c) evd in
+           let evd' = Evd.define evk c evd in
 	     check_evar_instance evd' evk c conv_algo
 	 else evd
       | l when List.length l < List.length l' ->
@@ -1401,8 +1394,8 @@ let occur_evar_upto_types sigma n c =
          Array.iter occur_rec args
        else (
          seen := Evar.Set.add sp !seen;
-	 Option.iter occur_rec (existential_opt_value sigma e);
-	 occur_rec (Evd.existential_type sigma e))
+         Option.iter occur_rec (existential_opt_value0 sigma e);
+         occur_rec (Evd.existential_type0 sigma e))
     | _ -> Constr.iter occur_rec c
   in
   try occur_rec c; false with Occur -> true
@@ -1529,7 +1522,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
              (* Try to project (a restriction of) the left evar ... *)
             try
               let evd,body = project_evar_on_evar false conv_algo env' evd aliases 0 None ev'' ev' in
-              let evd = Evd.define evk' (EConstr.Unsafe.to_constr body) evd in
+              let evd = Evd.define evk' body evd in
 		check_evar_instance evd evk' body conv_algo
             with
             | EvarSolvedOnTheFly _ -> assert false (* ev has no candidates *)
@@ -1644,7 +1637,7 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
            print_constr body);
         raise e in*)
     let evd' = check_evar_instance evd' evk body conv_algo in
-    Evd.define evk (EConstr.Unsafe.to_constr body) evd'
+    Evd.define evk body evd'
   with
     | NotEnoughInformationToProgress sols ->
         postpone_non_unique_projection env evd pbty ev sols rhs
@@ -1691,8 +1684,6 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
  *)
 
 let status_changed evd lev (pbty,_,t1,t2) =
-  let t1 = EConstr.of_constr t1 in
-  let t2 = EConstr.of_constr t2 in
   (try Evar.Set.mem (head_evar evd t1) lev with NoHeadEvar -> false) ||
   (try Evar.Set.mem (head_evar evd t2) lev with NoHeadEvar -> false)
 
@@ -1702,7 +1693,7 @@ let reconsider_unif_constraints conv_algo evd =
     (fun p (pbty,env,t1,t2 as x) ->
        match p with
        | Success evd ->
-           (match conv_algo env evd pbty (EConstr.of_constr t1) (EConstr.of_constr t2) with
+           (match conv_algo env evd pbty t1 t2 with
            | Success _ as x -> x
            | UnifFailure (i,e) -> UnifFailure (i,CannotSolveConstraint (x,e)))
        | UnifFailure _ as x -> x)
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index fcbf50fea..85911394f 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -401,9 +401,9 @@ and nf_evar env sigma evk ty args =
     mkEvar (evk, Array.of_list args), ty
 
 let evars_of_evar_map sigma =
-  { Nativelambda.evars_val = Evd.existential_opt_value sigma;
-    Nativelambda.evars_typ = Evd.existential_type sigma;
-    Nativelambda.evars_metas = Evd.meta_type sigma }
+  { Nativelambda.evars_val = Evd.existential_opt_value0 sigma;
+    Nativelambda.evars_typ = Evd.existential_type0 sigma;
+    Nativelambda.evars_metas = Evd.meta_type0 sigma }
 
 (* fork perf process, return profiler's process id *)
 let start_profiler_linux profile_fn =
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index e52112fda..27e457e3b 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -184,7 +184,7 @@ let pattern_of_constr env sigma t =
       | Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ ->
         (* These are the two evar kinds used for existing goals *)
         (* see Proofview.mark_in_evm *)
-         if Evd.is_defined sigma evk then pattern_of_constr env (Evd.existential_value sigma ev)
+         if Evd.is_defined sigma evk then pattern_of_constr env (Evd.existential_value0 sigma ev)
          else PEvar (evk,Array.map (pattern_of_constr env) ctxt)
       | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false
       | _ -> 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 2c371d5cf..947469ca0 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -315,7 +315,7 @@ let apply_inference_hook hook evdref frozen = match frozen with
     then
       try
         let sigma, c = hook sigma evk in
-        Evd.define evk (EConstr.Unsafe.to_constr c) sigma
+        Evd.define evk c sigma
       with Exit ->
         sigma
     else
@@ -532,7 +532,7 @@ let pretype_global ?loc rigid env evd gr us =
        interp_instance ?loc evd ~len l
   in
   let (sigma, c) = Evd.fresh_global ?loc ~rigid ?names:instance env.ExtraEnv.env evd gr in
-  (sigma, EConstr.of_constr c)
+  (sigma, c)
 
 let pretype_ref ?loc evdref env ref us =
   match ref with
@@ -1109,7 +1109,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
   let f decl (subst,update) =
     let id = NamedDecl.get_id decl in
-    let t = replace_vars subst (EConstr.of_constr (NamedDecl.get_type decl)) in
+    let t = replace_vars subst (NamedDecl.get_type decl) in
     let c, update =
       try
         let c = List.assoc id update in
@@ -1150,7 +1150,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match D
            (* Correction of bug #5315 : we need to define an evar for *all* holes *)
            let evkt = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s) in
            let ev,_ = destEvar !evdref evkt in
-           evdref := Evd.define ev (to_constr ~abort_on_undefined_evars:false !evdref v) !evdref;
+           evdref := Evd.define ev (nf_evar !evdref v) !evdref;
            (* End of correction of bug #5315 *)
            { utj_val = v;
 	     utj_type = s }
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 360c6e86e..244b8e60b 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -871,7 +871,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
     | Evar ev -> fold ()
     | Meta ev ->
       (match safe_meta_value sigma ev with
-      | Some body -> whrec cst_l (EConstr.of_constr body, stack)
+      | Some body -> whrec cst_l (body, stack)
       | None -> fold ())
     | Const (c,u as const) ->
       reduction_effect_hook env sigma (EConstr.to_constr sigma x)
@@ -1106,7 +1106,7 @@ let local_whd_state_gen flags sigma =
     | Evar ev -> s
     | Meta ev ->
       (match safe_meta_value sigma ev with
-        Some c -> whrec (EConstr.of_constr c,stack)
+        Some c -> whrec (c,stack)
       | None -> s)
 
     | Construct ((ind,c),u) ->
@@ -1392,7 +1392,7 @@ let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 =
 (********************************************************************)
 
 let whd_meta sigma c = match EConstr.kind sigma c with
-  | Meta p -> (try EConstr.of_constr (meta_value sigma p) with Not_found -> c)
+  | Meta p -> (try meta_value sigma p with Not_found -> c)
   | _ -> c
 
 let default_plain_instance_ident = Id.of_string "H"
@@ -1612,7 +1612,7 @@ let meta_value evd mv =
     match meta_opt_fvalue evd mv with
     | Some (b,_) ->
       let metas = Metamap.bind valrec b.freemetas in
-      instance evd metas (EConstr.of_constr b.rebus)
+      instance evd metas b.rebus
     | None -> mkMeta mv
   in
   valrec mv
@@ -1625,9 +1625,8 @@ let meta_instance sigma b =
     instance sigma c_sigma b.rebus
 
 let nf_meta sigma c =
-  let c = EConstr.Unsafe.to_constr c in
   let cl = mk_freelisted c in
-  meta_instance sigma { cl with rebus = EConstr.of_constr cl.rebus }
+  meta_instance sigma { cl with rebus = cl.rebus }
 
 (* Instantiate metas that create beta/iota redexes *)
 
@@ -1648,7 +1647,6 @@ let meta_reducible_instance evd b =
 	(match
 	  try
 	    let g, s = Metamap.find m metas in
-	    let g = EConstr.of_constr g in
             let is_coerce = match s with CoerceToType -> true | _ -> false in
 	    if isConstruct evd g || not is_coerce then Some g else None
 	  with Not_found -> None
@@ -1660,7 +1658,6 @@ let meta_reducible_instance evd b =
 	(match
 	  try
 	    let g, s = Metamap.find m metas in
-	    let g = EConstr.of_constr g in
             let is_coerce = match s with CoerceToType -> true | _ -> false in
 	    if isLambda evd g || not is_coerce then Some g else None
 	  with Not_found -> None
@@ -1669,7 +1666,6 @@ let meta_reducible_instance evd b =
 	   | None -> mkApp (f,Array.map irec l))
     | Meta m ->
 	(try let g, s = Metamap.find m metas in
-          let g = EConstr.of_constr g in
           let is_coerce = match s with CoerceToType -> true | _ -> false in
           if not is_coerce then irec g else u
 	 with Not_found -> u)
@@ -1678,7 +1674,6 @@ let meta_reducible_instance evd b =
 	  (match
 	  try
 	    let g, s = Metamap.find m metas in
-            let g = EConstr.of_constr g in
             let is_coerce = match s with CoerceToType -> true | _ -> false in
 	    if isConstruct evd g || not is_coerce then Some g else None
 	  with Not_found -> None
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 95aa5ebef..746a68b21 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -57,8 +57,8 @@ let get_type_from_constraints env sigma t =
   if isEvar sigma (fst (decompose_app_vect sigma t)) then
     match
       List.map_filter (fun (pbty,env,t1,t2) ->
-        if is_fconv Reduction.CONV env sigma t (EConstr.of_constr t1) then Some t2
-        else if is_fconv Reduction.CONV env sigma t (EConstr.of_constr t2) then Some t1
+        if is_fconv Reduction.CONV env sigma t t1 then Some t2
+        else if is_fconv Reduction.CONV env sigma t t2 then Some t1
         else None)
         (snd (Evd.extract_all_conv_pbs sigma))
     with
@@ -99,7 +99,7 @@ let retype ?(polyprop=true) sigma =
   let rec type_of env cstr =
     match EConstr.kind sigma cstr with
     | Meta n ->
-      (try strip_outer_cast sigma (EConstr.of_constr (Evd.meta_ftype sigma n).Evd.rebus)
+      (try strip_outer_cast sigma (Evd.meta_ftype sigma n).Evd.rebus
        with Not_found -> retype_error (BadMeta n))
     | Rel n ->
 	let ty = RelDecl.get_type (lookup_rel n env) in
@@ -115,7 +115,7 @@ let retype ?(polyprop=true) sigma =
           try Inductiveops.find_rectype env sigma t
           with Not_found ->
           try
-            let t = EConstr.of_constr (get_type_from_constraints env sigma t) in
+            let t = get_type_from_constraints env sigma t in
             Inductiveops.find_rectype env sigma t
           with Not_found -> retype_error BadRecursiveType
         in
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 977713fd8..696001ab7 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -416,7 +416,7 @@ exception Partial
    reduction is solved by the expanded fix term. *)
 let solve_arity_problem env sigma fxminargs c =
   let evm = ref sigma in
-  let set_fix i = evm := Evd.define i (Constr.mkVar vfx) !evm in
+  let set_fix i = evm := Evd.define i (mkVar vfx) !evm in
   let rec check strict c =
     let c' = whd_betaiotazeta sigma c in
     let (h,rcargs) = decompose_app_vect sigma c' in
@@ -641,7 +641,7 @@ let whd_nothing_for_iota env sigma s =
 	     | _ -> s)
       | Evar ev -> s
       | Meta ev ->
-	(try whrec (EConstr.of_constr (Evd.meta_value sigma ev), stack)
+        (try whrec (Evd.meta_value sigma ev, stack)
 	with Not_found -> s)
       | Const (const, u) when is_transparent_constant full_transparent_state const ->
           let u = EInstance.kind sigma u in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 08051fd3a..30ddeffa6 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -158,7 +158,7 @@ let rec is_class_type evd c =
     | _ -> is_class_constr evd c
       
 let is_class_evar evd evi =
-  is_class_type evd (EConstr.of_constr evi.Evd.evar_concl)
+  is_class_type evd evi.Evd.evar_concl
 
 (*
  * classes persistent object
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index c4eb6af89..aaec73f04 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -29,7 +29,6 @@ let meta_type evd mv =
   let ty =
     try Evd.meta_ftype evd mv
     with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv) ++ str ".") in
-  let ty = Evd.map_fl EConstr.of_constr ty in
   meta_instance evd ty
 
 let inductive_type_knowing_parameters env sigma (ind,u) jl =
@@ -129,7 +128,7 @@ let e_is_correct_arity env evdref c pj ind specif params =
         then error ()
     | Evar (ev,_), [] ->
         let evd, s = Evd.fresh_sort_in_family env !evdref (max_sort allowed_sorts) in
-        evdref := Evd.define ev (Constr.mkSort s) evd
+        evdref := Evd.define ev (mkSort s) evd
     | _, (LocalDef _ as d)::ar' ->
         srec (push_rel d env) (lift 1 pt') ar'
     | _ ->
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index ca03b96ab..d98ce9aba 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -84,7 +84,7 @@ let occur_meta_or_undefined_evar evd c =
     | Evar (ev,args) ->
         (match evar_body (Evd.find evd ev) with
         | Evar_defined c ->
-            occrec c; Array.iter occrec args
+            occrec (EConstr.Unsafe.to_constr c); Array.iter occrec args
         | Evar_empty -> raise Occur)
     | _ -> Constr.iter occrec c
   in try occrec c; false with Occur | Not_found -> true
@@ -189,10 +189,9 @@ let pose_all_metas_as_evars env evd t =
   let rec aux t = match EConstr.kind !evdref t with
   | Meta mv ->
       (match Evd.meta_opt_fvalue !evdref mv with
-       | Some ({rebus=c},_) -> EConstr.of_constr c
+       | Some ({rebus=c},_) -> c
        | None ->
         let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in
-        let ty = EConstr.of_constr ty in
         let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in
         let ty =
           if Flags.version_strictly_greater Flags.V8_6
@@ -200,7 +199,7 @@ let pose_all_metas_as_evars env evd t =
           else ty (* some beta-iota-normalization "regression" in 8.5 and 8.6 *) in
         let src = Evd.evar_source_of_meta mv !evdref in
         let ev = Evarutil.e_new_evar env evdref ~src ty in
-        evdref := meta_assign mv (EConstr.Unsafe.to_constr ev,(Conv,TypeNotProcessed)) !evdref;
+        evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) !evdref;
         ev)
   | _ ->
       EConstr.map !evdref aux t in
@@ -1060,7 +1059,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
                 (evd,t2::ks, m-1)
             else
               let mv = new_meta () in
-	      let evd' = meta_declare mv (EConstr.Unsafe.to_constr (substl ks b)) evd in
+              let evd' = meta_declare mv (substl ks b) evd in
 	      (evd', mkMeta mv :: ks, m - 1))
 	  (sigma,[],List.length bs) bs
       in
@@ -1247,7 +1246,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 env evd j tycon in
   let evd' = Evarconv.solve_unif_constraints_with_heuristics env evd' in
-  let evd' = Evd.map_metas_fvalue (fun c -> EConstr.Unsafe.to_constr (nf_evar evd' (EConstr.of_constr c))) evd' in
+  let evd' = Evd.map_metas_fvalue (fun c -> nf_evar evd' c) evd' in
     (evd',j'.uj_val)
 
 let w_coerce_to_type env evd c cty mvty =
@@ -1359,11 +1358,11 @@ let w_merge env with_types flags (evd,metas,evars : subst0) =
 	  if meta_defined evd mv then
 	    let {rebus=c'},(status',_) = meta_fvalue evd mv in
             let (take_left,st,(evd,metas',evars')) =
-	      merge_instances env evd flags status' status (EConstr.of_constr c') c
+              merge_instances env evd flags status' status c' c
 	    in
 	    let evd' =
               if take_left then evd
-              else meta_reassign mv (EConstr.Unsafe.to_constr c,(st,TypeProcessed)) evd
+              else meta_reassign mv (c,(st,TypeProcessed)) evd
 	    in
               w_merge_rec evd' (metas'@metas@metas'') (evars'@evars'') eqns
     	  else
@@ -1372,7 +1371,7 @@ let w_merge env with_types flags (evd,metas,evars : subst0) =
                 if isMetaOf evd mv (whd_all env evd c) then evd
                 else error_cannot_unify env evd (mkMeta mv,c)
               else
-	        meta_assign mv (EConstr.Unsafe.to_constr c,(status,TypeProcessed)) evd in
+                meta_assign mv (c,(status,TypeProcessed)) evd in
 	    w_merge_rec evd' (metas''@metas) evars'' eqns
     | [] ->
 	(* Process type eqns *)
@@ -1396,17 +1395,17 @@ let w_merge env with_types flags (evd,metas,evars : subst0) =
     let (evd', c) = applyHead sp_env evd nargs hdc in
     let (evd'',mc,ec) =
       unify_0 sp_env evd' CUMUL flags
-        (get_type_of sp_env evd' c) (EConstr.of_constr ev.evar_concl) in
+        (get_type_of sp_env evd' c) ev.evar_concl in
     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 (EConstr.Unsafe.to_constr (Evarutil.nf_evar evd''' c)) evd''' in
+    then Evd.define sp c evd'''
+    else Evd.define sp (Evarutil.nf_evar evd''' c) evd''' in
 
   let check_types evd = 
     let metas = Evd.meta_list evd in
     let eqns = List.fold_left (fun acc (mv, b) ->
       match b with
-      | Clval (n, (t, (c, TypeNotProcessed)), v) -> (mv, c, EConstr.of_constr t.rebus) :: acc
+      | Clval (n, (t, (c, TypeNotProcessed)), v) -> (mv, c, t.rebus) :: acc
       | _ -> acc) [] metas
     in w_merge_rec evd [] [] eqns
   in
@@ -1417,11 +1416,6 @@ let w_merge env with_types flags (evd,metas,evars : subst0) =
   in
   if with_types then check_types res else res
 
-let retract_coercible_metas evd =
-  let (metas, evd) = retract_coercible_metas evd in
-  let map (mv, c, st) = (mv, EConstr.of_constr c, st) in
-  (List.map map metas, evd)
-
 let w_unify_meta_types env ?(flags=default_unify_flags ()) evd =
   let metas,evd = retract_coercible_metas evd in
   w_merge env true flags.merge_unify_flags (evd,metas,[])
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index f314ae0d6..049c3aff5 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -205,7 +205,7 @@ and nf_univ_args ~nb_univs mk env sigma stk =
 and nf_evar env sigma evk stk =
   let evi = try Evd.find sigma evk with Not_found -> assert false in
   let hyps = Environ.named_context_of_val (Evd.evar_filtered_hyps evi) in
-  let concl = Evd.evar_concl evi in
+  let concl = EConstr.Unsafe.to_constr @@ Evd.evar_concl evi in
   if List.is_empty hyps then
     nf_stk env sigma (mkEvar (evk, [||])) concl stk
   else match stk with