Removing compatibility layers in Retyping

15 files changed, 73 insertions, 86 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 01e2db08cb..565a9725c2 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1502,7 +1502,7 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest =
   if not (Flags.is_program_mode ()) && (isRel sigma orig || isVar sigma orig) then
     (* Try to compile first using non expanded alias *)
     try
-      if initial then f orig (EConstr.of_constr (Retyping.get_type_of pb.env sigma orig))
+      if initial then f orig (Retyping.get_type_of pb.env sigma orig)
       else just_pop ()
     with e when precatchable_exception e ->
     (* Try then to compile using expanded alias *)
@@ -1517,7 +1517,7 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest =
     (* Could be needed in case of a recursive call which requires to
        be on a variable for size reasons *)
     pb.evdref := sigma;
-    if initial then f orig (EConstr.of_constr (Retyping.get_type_of pb.env !(pb.evdref) orig))
+    if initial then f orig (Retyping.get_type_of pb.env !(pb.evdref) orig)
     else just_pop ()
 
 
@@ -1650,13 +1650,12 @@ let abstract_tycon loc env evdref subst tycon extenv t =
     | Rel n when is_local_def (lookup_rel n env) -> t
     | Evar ev ->
         let ty = get_type_of env !evdref t in
-	let ty = Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref (EConstr.of_constr ty) in
+	let ty = Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty in
         let inst =
 	  List.map_i
 	    (fun i _ ->
               try list_assoc_in_triple i subst0 with Not_found -> mkRel i)
               1 (rel_context env) in
-        let ty = EConstr.of_constr ty in
         let ev' = e_new_evar env evdref ~src ty in
         begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,substl inst ev') with
         | Success evd -> evdref := evd
@@ -1672,10 +1671,8 @@ let abstract_tycon loc env evdref subst tycon extenv t =
       let vl = List.map pi1 good in
       let ty = 
 	let ty = get_type_of env !evdref t in
-	let ty = EConstr.of_constr ty in
 	  Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty
       in
-      let ty = EConstr.of_constr ty in
       let ty = lift (-k) (aux x ty) in
       let depvl = free_rels !evdref ty in
       let inst =
@@ -1708,7 +1705,6 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t =
     | Some t ->
         let t = abstract_tycon loc tycon_env evdref subst tycon extenv t in
         let evd,tt = Typing.type_of extenv !evdref t in
-        let tt = EConstr.of_constr tt in
         evdref := evd;
         (t,tt) in
   let b = e_cumul env evdref tt (mkSort s) (* side effect *) in
@@ -2109,7 +2105,6 @@ let constr_of_pat env evdref arsign pat avoid =
 	let app = applist (cstr, List.map (lift (List.length sign)) params) in
 	let app = applist (app, args) in
 	let apptype = Retyping.get_type_of env ( !evdref) app in
-	let apptype = EConstr.of_constr apptype in
 	let IndType (indf, realargs) = find_rectype env (!evdref) apptype in
 	  match alias with
 	      Anonymous ->
@@ -2370,7 +2365,6 @@ let build_dependent_signature env evdref avoid tomatchs arsign =
 		    let t = RelDecl.get_type decl in
 		    let t = EConstr.of_constr t in
 		    let argt = Retyping.get_type_of env !evdref arg in
-                    let argt = EConstr.of_constr argt in
 		    let eq, refl_arg =
 		      if Reductionops.is_conv env !evdref argt t then
 			(mk_eq evdref (lift (nargeqs + slift) argt)
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index e4331aade2..13310c44d5 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -442,6 +442,7 @@ let cache_coercion (_, c) =
   let it, _ = class_info c.coercion_target in
   let value, ctx = Universes.fresh_global_instance (Global.env()) c.coercion_type in
   let typ = Retyping.get_type_of (Global.env ()) Evd.empty (EConstr.of_constr value) in
+  let typ = EConstr.Unsafe.to_constr typ in
   let xf =
     { coe_value = value;
       coe_type = typ;
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 7e85596308..f569d9fc4a 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -66,7 +66,7 @@ let apply_coercion_args env evd check isproj argl funj =
     | h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *)
       match EConstr.kind !evdref (whd_all env !evdref typ) with
       | Prod (_,c1,c2) ->
-        if check && not (e_cumul env evdref (EConstr.of_constr (Retyping.get_type_of env !evdref h)) c1) then
+        if check && not (e_cumul env evdref (Retyping.get_type_of env !evdref h) c1) then
 	  raise NoCoercion;
         apply_rec (h::acc) (subst1 h c2) restl
       | _ -> anomaly (Pp.str "apply_coercion_args")
@@ -498,7 +498,7 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
 	  let v2 = Option.map (fun v -> beta_applist evd' (lift 1 v,[v1])) v in
 	  let t2 = match v2 with
 	    | None -> subst_term evd' v1 t2
-	    | Some v2 -> EConstr.of_constr (Retyping.get_type_of env1 evd' v2) in
+	    | Some v2 -> Retyping.get_type_of env1 evd' v2 in
 	  let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in
 	    (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2')
       | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e))
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 3d5a5f0259..d4e156fa4b 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -504,7 +504,7 @@ let rec detype flags avoid env sigma t =
 	      let pb = Environ.lookup_projection p (snd env) in
 	      let body = pb.Declarations.proj_body in
 	      let ty = Retyping.get_type_of (snd env) sigma (EConstr.of_constr c) in
-	      let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma (EConstr.of_constr ty) in
+	      let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma ty in
 	      let args = List.map EConstr.Unsafe.to_constr args in
 	      let body' = strip_lam_assum body in
 	      let body' = subst_instance_constr u body' in
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6dce8627da..afb0bf6d5a 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -168,7 +168,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
     | Some c -> (* A primitive projection applied to c *)
       let ty = Retyping.get_type_of ~lax:true env sigma c in
       let (i,u), ind_args = 
-	try Inductiveops.find_mrectype env sigma (EConstr.of_constr ty)
+	try Inductiveops.find_mrectype env sigma ty
 	with _ -> raise Not_found
       in Stack.append_app_list ind_args Stack.empty, c, sk1
     | None ->
@@ -882,7 +882,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
       List.fold_left
 	(fun (i,ks,m,test) b ->
 	  if match n with Some n -> Int.equal m n | None -> false then
-	    let ty = EConstr.of_constr (Retyping.get_type_of env i t2) in
+	    let ty = Retyping.get_type_of env i t2 in
 	    let test i = evar_conv_x trs env i CUMUL ty (substl ks b) in
 	      (i,t2::ks, m-1, test)
 	  else
@@ -1052,7 +1052,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
       let id = NamedDecl.get_id decl' in
       let t = EConstr.of_constr (NamedDecl.get_type decl') in
       let evs = ref [] in
-      let ty = EConstr.of_constr (Retyping.get_type_of env_rhs evd c) in
+      let ty = Retyping.get_type_of env_rhs evd c in
       let filter' = filter_possible_projections evd c ty ctxt args in
       (id,t,c,ty,evs,Filter.make filter',occs) :: make_subst (ctxt',l,occsl)
   | _, _, [] -> []
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 3003620d7e..de2e46a781 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -23,6 +23,14 @@ open Evarutil
 open Pretype_errors
 open Sigma.Notations
 
+let nlocal_assum (na, t) =
+  let inj = EConstr.Unsafe.to_constr in
+  Context.Named.Declaration.LocalAssum (na, inj t)
+
+let nlocal_def (na, b, t) =
+  let inj = EConstr.Unsafe.to_constr in
+  Context.Named.Declaration.LocalDef (na, inj b, inj t)
+
 let normalize_evar evd ev =
   match EConstr.kind evd (mkEvar ev) with
   | Evar (evk,args) -> (evk,args)
@@ -108,11 +116,11 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
       | Some dir -> refresh status dir t)
     else (refresh_term_evars false true t; t)
   in
-    if !modified then !evdref, EConstr.Unsafe.to_constr t' else !evdref, EConstr.Unsafe.to_constr t
+    if !modified then !evdref, t' else !evdref, t
 
 let get_type_of_refresh ?(polyprop=true) ?(lax=false) env sigma c =
   let ty = Retyping.get_type_of ~polyprop ~lax env sigma c in
-    refresh_universes (Some false) env sigma (EConstr.of_constr ty)
+    refresh_universes (Some false) env sigma ty
 		      
 
 (************************)
@@ -146,7 +154,7 @@ let recheck_applications conv_algo env evdref t =
     | App (f, args) ->
        let () = aux env f in
        let fty = Retyping.get_type_of env !evdref f in
-       let argsty = Array.map (fun x -> aux env x; EConstr.of_constr (Retyping.get_type_of env !evdref x)) args in
+       let argsty = Array.map (fun x -> aux env x; Retyping.get_type_of env !evdref x) args in
        let rec aux i ty =
 	 if i < Array.length argsty then
 	 match EConstr.kind !evdref (whd_all env !evdref ty) with
@@ -158,7 +166,7 @@ let recheck_applications conv_algo env evdref t =
 		Pretype_errors.error_cannot_unify env evd ~reason (argsty.(i), dom))
 	 | _ -> raise (IllTypedInstance (env, ty, argsty.(i)))
        else ()
-     in aux 0 (EConstr.of_constr fty)
+     in aux 0 fty
     | _ ->
        iter_with_full_binders !evdref (fun d env -> push_rel d env) aux env t
   in aux env t
@@ -173,7 +181,7 @@ type 'a update =
 | NoUpdate
 
 open Context.Named.Declaration
-let inst_of_vars sign = Array.map_of_list (get_id %> EConstr.mkVar) sign
+let inst_of_vars sign = Array.map_of_list (get_id %> mkVar) sign
 
 let restrict_evar_key evd evk filter candidates =
   match filter, candidates with
@@ -413,9 +421,9 @@ let free_vars_and_rels_up_alias_expansion sigma aliases c =
 
 let rec expand_and_check_vars sigma aliases = function
   | [] -> []
-  | a::l when EConstr.isRel sigma a || EConstr.isVar sigma a ->
+  | a::l when isRel sigma a || isVar sigma a ->
       let a = expansion_of_var sigma aliases a in
-      if EConstr.isRel sigma a || EConstr.isVar sigma a then a :: expand_and_check_vars sigma aliases l
+      if isRel sigma a || isVar sigma a then a :: expand_and_check_vars sigma aliases l
       else raise Exit
   | _ ->
       raise Exit
@@ -480,7 +488,7 @@ let is_unification_pattern_meta env evd nb m l t =
   (* so we need to be a rel <= nb *)
   if List.for_all (fun x -> isRel evd x && destRel evd x <= nb) l then
     match find_unification_pattern_args env evd l t with
-    | Some _ as x when not (dependent evd (EConstr.mkMeta m) t) -> x
+    | Some _ as x when not (dependent evd (mkMeta m) t) -> x
     | _ -> None
   else
     None
@@ -591,15 +599,15 @@ let make_projectable_subst aliases sigma evi args =
 
 let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_sign sign filter inst_in_env =
   let evd = Sigma.Unsafe.of_evar_map evd in
-  let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd (EConstr.of_constr ty_t_in_sign) ~filter ~src inst_in_env 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 (evk, _) = destEvar evd evar_in_env in
-  let evd = define_fun env evd None (EConstr.destEvar evd evar_in_env) t_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,whd_evar evd (EConstr.Unsafe.to_constr evar_in_sign))
+  (evd,EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr 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
@@ -624,7 +632,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
   if Evd.is_defined evd evk1 then
       (* Some circularity somewhere (see e.g. #3209) *)
       raise MorePreciseOccurCheckNeeeded;
-  let (evk1,args1) = EConstr.destEvar evd (EConstr.mkEvar (evk1,args1)) in
+  let (evk1,args1) = destEvar evd (mkEvar (evk1,args1)) in
   let evi1 = Evd.find_undefined evd evk1 in
   let env1,rel_sign = env_rel_context_chop k env in
   let sign1 = evar_hyps evi1 in
@@ -641,16 +649,16 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
         let t_in_env = EConstr.of_constr t_in_env in
         let s = Retyping.get_sort_of env evd t_in_env in
         let evd,ty_t_in_sign = refresh_universes
-	 ~status:univ_flexible (Some false) env evd (EConstr.mkSort s) in
+	 ~status:univ_flexible (Some false) env evd (mkSort s) in
         define_evar_from_virtual_equation define_fun env evd src t_in_env
           ty_t_in_sign sign filter inst_in_env in
       let evd,d' = match d with
-      | LocalAssum _ -> evd, Context.Named.Declaration.LocalAssum (id,t_in_sign)
+      | LocalAssum _ -> evd, nlocal_assum (id,t_in_sign)
       | LocalDef (_,b,_) ->
           let b = EConstr.of_constr b in
           let evd,b = define_evar_from_virtual_equation define_fun env evd src b
             t_in_sign sign filter inst_in_env in
-          evd, Context.Named.Declaration.LocalDef (id,b,t_in_sign) in
+          evd, nlocal_def (id,b,t_in_sign) in
       (push_named_context_val d' sign, Filter.extend 1 filter,
        (mkRel 1)::(List.map (lift 1) inst_in_env),
        (mkRel 1)::(List.map (lift 1) inst_in_sign),
@@ -661,11 +669,10 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
   let evd,ev2ty_in_sign =
     let s = Retyping.get_sort_of env evd ty_in_env in
     let evd,ty_t_in_sign = refresh_universes
-     ~status:univ_flexible (Some false) env evd (EConstr.mkSort s) in
+     ~status:univ_flexible (Some false) env evd (mkSort s) in
     define_evar_from_virtual_equation define_fun env evd src ty_in_env
       ty_t_in_sign sign2 filter2 inst2_in_env in
   let evd = Sigma.Unsafe.of_evar_map evd in
-  let ev2ty_in_sign = EConstr.of_constr ev2ty_in_sign in
   let Sigma (ev2_in_sign, evd, _) =
     new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src inst2_in_sign in
   let evd = Sigma.to_evar_map evd in
@@ -899,7 +906,7 @@ let extract_unique_projection = function
 let extract_candidates sols =
   try
     UpdateWith
-      (List.map (function (id,ProjectVar) -> EConstr.mkVar id | _ -> raise Exit) sols)
+      (List.map (function (id,ProjectVar) -> mkVar id | _ -> raise Exit) sols)
   with Exit ->
     NoUpdate
 
@@ -1171,7 +1178,7 @@ let check_evar_instance evd evk1 body conv_algo =
   (* FIXME: The body might be ill-typed when this is called from w_merge *)
   (* This happens in practice, cf MathClasses build failure on 2013-3-15 *)
   let ty =
-    try EConstr.of_constr (Retyping.get_type_of ~lax:true evenv evd body)
+    try Retyping.get_type_of ~lax:true evenv evd body
     with Retyping.RetypeError _ -> error "Ill-typed evar instance"
   in
   match conv_algo evenv evd Reduction.CUMUL ty (EConstr.of_constr evi.evar_concl) with
@@ -1378,7 +1385,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
         | (id,p)::_::_ ->
             if choose then (mkVar id, p) else raise (NotUniqueInType sols)
       in
-      let ty = lazy (EConstr.of_constr (Retyping.get_type_of env !evdref t)) in
+      let ty = lazy (Retyping.get_type_of env !evdref t) in
       let evd = do_projection_effects (evar_define conv_algo ~choose) env ty !evdref p in
       evdref := evd;
       c
@@ -1440,7 +1447,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
           if not !progress then
             raise (NotEnoughInformationEvarEvar t);
           (* Make the virtual left evar real *)
-          let ty = EConstr.of_constr (get_type_of env' evd t) in
+          let ty = get_type_of env' evd t in
           let (evd,evar'',ev'') =
              materialize_evar (evar_define conv_algo ~choose) env' evd k ev ty in
           (* materialize_evar may instantiate ev' by another evar; adjust it *)
@@ -1474,7 +1481,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
           | _ -> None
         with
         | Some l ->
-            let ty = EConstr.of_constr (get_type_of env' !evdref t) in
+            let ty = get_type_of env' !evdref t in
             let candidates =
               try
                 let t =
@@ -1563,15 +1570,15 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
            str "----> " ++ int ev ++ str " := " ++
            print_constr body);
         raise e in*)
-    let evd' = check_evar_instance evd' evk (EConstr.of_constr body) conv_algo in
-    Evd.define evk body evd'
+    let evd' = check_evar_instance evd' evk body conv_algo in
+    Evd.define evk (EConstr.Unsafe.to_constr body) evd'
   with
     | NotEnoughInformationToProgress sols ->
         postpone_non_unique_projection env evd pbty ev sols rhs
     | NotEnoughInformationEvarEvar t ->
-        add_conv_oriented_pb (pbty,env,EConstr.mkEvar ev,t) evd
+        add_conv_oriented_pb (pbty,env,mkEvar ev,t) evd
     | MorePreciseOccurCheckNeeeded ->
-        add_conv_oriented_pb (pbty,env,EConstr.mkEvar ev,rhs) evd
+        add_conv_oriented_pb (pbty,env,mkEvar ev,rhs) evd
     | NotInvertibleUsingOurAlgorithm _ | MetaOccurInBodyInternal as e ->
         raise e
     | OccurCheckIn (evd,rhs) ->
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index b83147514b..f2102f8cd1 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -42,7 +42,7 @@ val refresh_universes :
   (* Also refresh Prop and Set universes, so that the returned type can be any supertype
      of the original type *)
   bool option (* direction: true for levels lower than the existing levels *) ->
-  env -> evar_map -> types -> evar_map * Constr.types
+  env -> evar_map -> types -> evar_map * types
 
 val solve_refl : ?can_drop:bool -> conv_fun_bool -> env ->  evar_map ->
   bool option -> existential_key -> constr array -> constr array -> evar_map
@@ -77,4 +77,4 @@ val remove_instance_local_defs :
   evar_map -> existential_key -> 'a array -> 'a list
 
 val get_type_of_refresh : 
-  ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> evar_map * Constr.types
+  ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> evar_map * types
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 7d2c96bb90..a0d8faab44 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -426,7 +426,7 @@ let invert_ltac_bound_name lvar env id0 id =
 		       str " which is not bound in current context.")
 
 let protected_get_type_of env sigma c =
-  try EConstr.of_constr (Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c)
+  try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c
   with Retyping.RetypeError _ ->
     user_err 
       (str "Cannot reinterpret " ++ quote (print_constr (EConstr.Unsafe.to_constr c)) ++
@@ -774,9 +774,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	       refreshed right away. *)
 	    let c = mkApp (f, args) in
 	    let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env.ExtraEnv.env) evdref c in
-	    let c = EConstr.of_constr c in
 	    let t = Retyping.get_type_of env.ExtraEnv.env !evdref c in
-	    let t = EConstr.of_constr t in
 	      make_judge c (* use this for keeping evars: resj.uj_val *) t
 	  else resj
       | _ -> resj 
@@ -840,7 +838,6 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
     let t = evd_comb1 (Evarsolve.refresh_universes
       ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env)
       evdref j.uj_type in
-    let t = EConstr.of_constr t in
     (* The name specified by ltac is used also to create bindings. So
        the substitution must also be applied on variables before they are
        looked up in the rel context. *)
@@ -1025,7 +1022,6 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
         let tval = evd_comb1 (Evarsolve.refresh_universes
                              ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env)
                           evdref tj.utj_val in
-        let tval = EConstr.of_constr tval in
 	let tval = nf_evar !evdref tval in
 	let cj, tval = match k with
 	  | VMcast ->
@@ -1097,7 +1093,6 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
            let s =
 	     let sigma =  !evdref in
 	     let t = Retyping.get_type_of env.ExtraEnv.env sigma v in
-	     let t = EConstr.of_constr t in
 	       match EConstr.kind sigma (whd_all env.ExtraEnv.env sigma t) with
                | Sort s -> s
                | Evar ev when is_Type (existential_type sigma ev) ->
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 7db30bf234..a9529d560c 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -109,7 +109,7 @@ let retype ?(polyprop=true) sigma =
         lift n ty
     | Var id -> type_of_var env id
     | Const cst -> EConstr.of_constr (rename_type_of_constant env cst)
-    | Evar (evk, args) -> EConstr.of_constr (Evd.existential_type sigma (evk, Array.map EConstr.Unsafe.to_constr args))
+    | Evar ev -> existential_type sigma ev
     | Ind ind -> EConstr.of_constr (rename_type_of_inductive env ind)
     | Construct cstr -> EConstr.of_constr (rename_type_of_constructor env cstr)
     | Case (_,p,c,lf) ->
@@ -210,7 +210,7 @@ let get_sort_of ?(polyprop=true) env sigma t =
 let get_sort_family_of ?(polyprop=true) env sigma c =
   let _,_,f,_ = retype ~polyprop sigma in anomaly_on_error (f env) c
 let type_of_global_reference_knowing_parameters env sigma c args =
-  let _,_,_,f = retype sigma in EConstr.Unsafe.to_constr (anomaly_on_error (f env c) args)
+  let _,_,_,f = retype sigma in anomaly_on_error (f env c) args
 
 let type_of_global_reference_knowing_conclusion env sigma c conclty =
   match EConstr.kind sigma c with
@@ -238,10 +238,10 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty =
 
 let get_type_of ?(polyprop=true) ?(lax=false) env sigma c =
   let f,_,_,_ = retype ~polyprop sigma in
-    if lax then EConstr.Unsafe.to_constr (f env c) else EConstr.Unsafe.to_constr (anomaly_on_error (f env) c)
+    if lax then f env c else anomaly_on_error (f env) c
 
 (* Makes an unsafe judgment from a constr *)
-let get_judgment_of env evc c = { uj_val = c; uj_type = EConstr.of_constr (get_type_of env evc c) }
+let get_judgment_of env evc c = { uj_val = c; uj_type = get_type_of env evc c }
 
 (* Returns sorts of a context *)
 let sorts_of_context env evc ctxt =
@@ -256,7 +256,7 @@ let sorts_of_context env evc ctxt =
 let expand_projection env sigma pr c args =
   let ty = get_type_of ~lax:true env sigma c in
   let (i,u), ind_args = 
-    try Inductiveops.find_mrectype env sigma (EConstr.of_constr ty) 
+    try Inductiveops.find_mrectype env sigma ty 
     with Not_found -> retype_error BadRecursiveType
   in
     mkApp (mkConstU (Projection.constant pr,u), 
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index a20b11b76e..ce9e1635fc 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -9,6 +9,7 @@
 open Term
 open Evd
 open Environ
+open EConstr
 
 (** This family of functions assumes its constr argument is known to be
    well-typable. It does not type-check, just recompute the type
@@ -26,25 +27,25 @@ type retype_error
 exception RetypeError of retype_error
 
 val get_type_of :
-  ?polyprop:bool -> ?lax:bool -> env -> evar_map -> EConstr.constr -> types
+  ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> types
 
 val get_sort_of :
-  ?polyprop:bool -> env -> evar_map -> EConstr.types -> sorts
+  ?polyprop:bool -> env -> evar_map -> types -> sorts
 
 val get_sort_family_of :
-  ?polyprop:bool -> env -> evar_map -> EConstr.types -> sorts_family
+  ?polyprop:bool -> env -> evar_map -> types -> sorts_family
 
 (** Makes an unsafe judgment from a constr *)
-val get_judgment_of : env -> evar_map -> EConstr.constr -> EConstr.unsafe_judgment
+val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment
 
-val type_of_global_reference_knowing_parameters : env -> evar_map -> EConstr.constr ->
-  EConstr.constr array -> types
+val type_of_global_reference_knowing_parameters : env -> evar_map -> constr ->
+  constr array -> types
 
 val type_of_global_reference_knowing_conclusion :
-  env -> evar_map -> EConstr.constr -> EConstr.types -> evar_map * EConstr.types
+  env -> evar_map -> constr -> types -> evar_map * types
 
 val sorts_of_context : env -> evar_map -> Context.Rel.t -> sorts list
 
-val expand_projection : env -> evar_map -> Names.projection -> EConstr.constr -> EConstr.constr list -> EConstr.constr
+val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr
 
 val print_retype_error : retype_error -> Pp.std_ppcmds
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 02524f8962..3fc01c86c6 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1148,7 +1148,6 @@ let compute = cbv_betadeltaiota
 
 let abstract_scheme env sigma (locc,a) (c, sigma) =
   let ta = Retyping.get_type_of env sigma a in
-  let ta = EConstr.of_constr ta in
   let na = named_hd env (EConstr.to_constr sigma ta) Anonymous in
   if occur_meta sigma ta then error "Cannot find a type for the generalisation.";
   if occur_meta sigma a then
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 9ee34341ba..9da7005e09 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -270,7 +270,7 @@ let add_class cl =
 let check_instance env sigma c =
   try 
     let (evd, c) = resolve_one_typeclass env sigma
-      (EConstr.of_constr (Retyping.get_type_of env sigma c)) in
+      (Retyping.get_type_of env sigma c) in
       not (Evd.has_undefined evd)
   with e when CErrors.noncritical e -> false
 
@@ -314,7 +314,7 @@ let build_subclasses ~check env sigma glob pri =
 	let declare_proj hints (cref, pri, body) =
 	  let path' = cref :: path in
 	  let ty = Retyping.get_type_of env sigma (EConstr.of_constr body) in
-	  let rest = aux pri body (EConstr.of_constr ty) path' in
+	  let rest = aux pri body ty path' in
 	    hints @ (path', pri, body) :: rest
 	in List.fold_left declare_proj [] projs 
   in
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index f67e0bddc7..d24160ea54 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -395,7 +395,7 @@ let type_of ?(refresh=false) env evd c =
   (* side-effect on evdref *)
     if refresh then
       Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type
-    else !evdref, EConstr.Unsafe.to_constr j.uj_type
+    else !evdref, j.uj_type
 
 let e_type_of ?(refresh=false) env evdref c =
   let env = enrich_env env evdref in
@@ -405,7 +405,7 @@ let e_type_of ?(refresh=false) env evdref c =
       let evd, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type in
       let () = evdref := evd in
       c
-    else EConstr.Unsafe.to_constr j.uj_type
+    else j.uj_type
 
 let e_solve_evars env evdref c =
   let env = enrich_env env evdref in
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 94a56b6e11..bf26358a22 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -19,10 +19,10 @@ val unsafe_type_of : env -> evar_map -> EConstr.constr -> types
 
 (** Typecheck a term and return its type + updated evars, optionally refreshing
     universes *)
-val type_of : ?refresh:bool -> env -> evar_map -> EConstr.constr -> evar_map * types
+val type_of : ?refresh:bool -> env -> evar_map -> EConstr.constr -> evar_map * EConstr.types
 
 (** Variant of [type_of] using references instead of state-passing. *)
-val e_type_of : ?refresh:bool -> env -> evar_map ref -> EConstr.constr -> types
+val e_type_of : ?refresh:bool -> env -> evar_map ref -> EConstr.constr -> EConstr.types
 
 (** Typecheck a type and return its sort *)
 val e_sort_of : env -> evar_map ref -> EConstr.types -> sorts
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 8a8649f111..233b58e91c 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -122,7 +122,6 @@ let abstract_list_all env evd typ c l =
         error_cannot_find_well_typed_abstraction env evd p l None
     | Pretype_errors.PretypeError (env',evd,TypingError x) ->
         error_cannot_find_well_typed_abstraction env evd p l (Some (env',x)) in
-  let typp = EConstr.of_constr typp in
   evd,(p,typp)
 
 let set_occurrences_of_last_arg args =
@@ -704,7 +703,6 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
 		(try
                    let tyM = Typing.meta_type sigma k in
                    let tyN = get_type_of curenv ~lax:true sigma cN in
-                   let tyN = EConstr.of_constr tyN in
                      check_compatibility curenv CUMUL flags substn tyN tyM
 		 with RetypeError _ ->
                    (* Renounce, maybe metas/evars prevents typing *) sigma)
@@ -724,7 +722,6 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
 	    if opt.with_types && flags.check_applied_meta_types then
               (try
                  let tyM = get_type_of curenv ~lax:true sigma cM in
-                 let tyM = EConstr.of_constr tyM in
                  let tyN = Typing.meta_type sigma k in
                    check_compatibility curenv CUMUL flags substn tyM tyN
                with RetypeError _ ->
@@ -911,8 +908,6 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
       try (* Force unification of the types to fill in parameters *)
 	let ty1 = get_type_of curenv ~lax:true sigma c1 in
 	let ty2 = get_type_of curenv ~lax:true sigma c2 in
-	let ty1 = EConstr.of_constr ty1 in
-	let ty2 = EConstr.of_constr ty2 in
 	  unify_0_with_initial_metas substn true curenv cv_pb
 	    { flags with modulo_conv_on_closed_terms = Some full_transparent_state;
 	      modulo_delta = full_transparent_state;
@@ -978,8 +973,6 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
 	     try (* Ensure we call conversion on terms of the same type *)
 	       let tyM = get_type_of curenv ~lax:true sigma m1 in
 	       let tyN = get_type_of curenv ~lax:true sigma n1 in
-	       let tyM = EConstr.of_constr tyM in
-	       let tyN = EConstr.of_constr tyN in
 	       check_compatibility curenv CUMUL flags substn tyM tyN
 	     with RetypeError _ ->
 	       (* Renounce, maybe metas/evars prevents typing *) sigma
@@ -1267,13 +1260,11 @@ let w_coerce_to_type env evd c cty mvty =
 let w_coerce env evd mv c =
   let cty = get_type_of env evd c in
   let mvty = Typing.meta_type evd mv in
-  w_coerce_to_type env evd c (EConstr.of_constr cty) mvty
+  w_coerce_to_type env evd c cty mvty
 
 let unify_to_type env sigma flags c status u =
   let sigma, c = refresh_universes (Some false) env sigma c in
-  let c = EConstr.of_constr c in
   let t = get_type_of env sigma (nf_meta sigma c) in
-  let t = EConstr.of_constr t in
   let t = nf_betaiota sigma (nf_meta sigma t) in
     unify_0 env sigma CUMUL flags t u
 
@@ -1406,7 +1397,7 @@ let w_merge env with_types flags (evd,metas,evars : subst0) =
     let evd' = Sigma.to_evar_map evd' in
     let (evd'',mc,ec) =
       unify_0 sp_env evd' CUMUL flags
-        (EConstr.of_constr (get_type_of sp_env evd' c)) (EConstr.of_constr ev.evar_concl) in
+        (get_type_of sp_env evd' c) (EConstr.of_constr 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'''
@@ -1458,13 +1449,13 @@ let check_types env flags (sigma,_,_ as subst) m n =
   if isEvar_or_Meta sigma (head_app sigma m) then
     unify_0_with_initial_metas subst true env CUMUL
       flags
-      (EConstr.of_constr (get_type_of env sigma n))
-      (EConstr.of_constr (get_type_of env sigma m))
+      (get_type_of env sigma n)
+      (get_type_of env sigma m)
   else if isEvar_or_Meta sigma (head_app sigma n) then
     unify_0_with_initial_metas subst true env CUMUL
       flags
-      (EConstr.of_constr (get_type_of env sigma m))
-      (EConstr.of_constr (get_type_of env sigma n))
+      (get_type_of env sigma m)
+      (get_type_of env sigma n)
   else subst
 
 let try_resolve_typeclasses env evd flag m n =
@@ -1595,7 +1586,6 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
         else t, [] in
       let sigma = w_typed_unify env sigma Reduction.CONV flags c t' in
       let ty = Retyping.get_type_of env sigma t in
-      let ty = EConstr.of_constr ty in
       if not (is_correct_type ty) then raise (NotUnifiable None);
       Some(sigma, t, l2)
     with
@@ -1628,8 +1618,8 @@ let make_eq_test env evd c =
 
 let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
   let id =
-    let ty = Option.map EConstr.Unsafe.to_constr ty in
     let t = match ty with Some t -> t | None -> get_type_of env sigma c in
+    let t = EConstr.Unsafe.to_constr t in
     let x = id_of_name_using_hdchar (Global.env()) t name in
     let ids = ids_of_named_context (named_context env) in
     if name == Anonymous then next_ident_away_in_goal x ids else