Eliminating parts of the right-hand side compatibility layer

16 files changed, 47 insertions, 62 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 119e92c82e..76ced2b1d6 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2335,7 +2335,7 @@ let abstract_tomatch env sigma tomatchs tycon =
 	     Rel n -> (lift lenctx c, lift_tomatch_type lenctx t) :: prev, ctx, names, tycon
 	   | _ ->
 	       let tycon = Option.map
-		 (fun t -> EConstr.of_constr (subst_term sigma (lift 1 c) (lift 1 t))) tycon in
+		 (fun t -> subst_term sigma (lift 1 c) (lift 1 t)) tycon in
 	       let name = next_ident_away (Id.of_string "filtered_var") names in
 		 (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev,
 	       local_def (Name name, lift lenctx c, lift lenctx $ type_of_tomatch t) :: ctx,
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index d67976232a..48f7be4bbb 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -502,8 +502,8 @@ 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 -> Retyping.get_type_of env1 evd' (EConstr.of_constr v2) in
-	  let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly (Option.map EConstr.of_constr v2) (EConstr.of_constr t2) u2 in
+	    | Some v2 -> EConstr.of_constr (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/constr_matching.ml b/pretyping/constr_matching.ml
index 06daa5116a..55612aa665 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -185,7 +185,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
        else false)
   in
   let rec sorec ctx env subst p t =
-    let cT = EConstr.of_constr (strip_outer_cast sigma t) in
+    let cT = strip_outer_cast sigma t in
     match p, EConstr.kind sigma cT with
       | PSoApp (n,args),m ->
         let fold (ans, seen) = function
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index c0611dcec8..87561868f7 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -267,7 +267,7 @@ let rec decomp_branch tags nal b (avoid,env as e) sigma c =
   | [] -> (List.rev nal,(e,c))
   | b::tags ->
       let na,c,f,body,t =
-        match kind_of_term (strip_outer_cast sigma (EConstr.of_constr c)), b with
+        match kind_of_term (EConstr.Unsafe.to_constr (strip_outer_cast sigma (EConstr.of_constr c))), b with
 	| Lambda (na,t,c),false -> na,c,compute_displayed_let_name_in,None,Some t
 	| LetIn (na,b,t,c),true ->
             na,c,compute_displayed_name_in,Some b,Some t
@@ -503,6 +503,7 @@ let rec detype flags avoid env sigma t =
 	      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 args = List.map EConstr.Unsafe.to_constr args in
 	      let body' = strip_lam_assum body in
 	      let body' = subst_instance_constr u body' in
 		substl (c :: List.rev args) body'
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index a968af7ff2..9675ae2ea9 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -170,7 +170,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
       let (i,u), ind_args = 
 	try Inductiveops.find_mrectype env sigma (EConstr.of_constr ty)
 	with _ -> raise Not_found
-      in Stack.append_app_list (List.map EConstr.of_constr ind_args) Stack.empty, c, sk1
+      in Stack.append_app_list ind_args Stack.empty, c, sk1
     | None ->
       match Stack.strip_n_app nparams sk1 with
       | Some (params1, c1, extra_args1) -> params1, c1, extra_args1
@@ -188,7 +188,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
   let t' = subst_univs_level_constr subst t' in
   let bs' = List.map (EConstr.of_constr %> subst_univs_level_constr subst) bs in
   let h, _ = decompose_app_vect sigma t' in
-    ctx',(EConstr.of_constr h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1),
+    ctx',(h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1),
     (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1,
     (n, Stack.zip sigma (t2,sk2))
 
@@ -907,7 +907,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
        (fun i -> exact_ise_stack2 env i (evar_conv_x trs) sk1 sk2);
        test;
        (fun i -> evar_conv_x trs env i CONV h2
-	 (EConstr.of_constr (fst (decompose_app_vect i (substl ks h)))))]
+	 (fst (decompose_app_vect i (substl ks h))))]
   else UnifFailure(evd,(*dummy*)NotSameHead)
 
 and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 7725719261..65b6d287d5 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -518,7 +518,6 @@ let is_unification_pattern (env,nb) evd f l t =
 let solve_pattern_eqn env sigma l c =
   let c' = List.fold_right (fun a c ->
     let c' = subst_term sigma (lift 1 a) (lift 1 c) in
-    let c' = EConstr.of_constr c' in
     match EConstr.kind sigma a with
       (* Rem: if [a] links to a let-in, do as if it were an assumption *)
       | Rel n ->
@@ -557,7 +556,7 @@ let make_projectable_subst aliases sigma evi args =
         | LocalAssum (id,c), a::rest ->
             let cstrs =
               let a',args = decompose_app_vect sigma a in
-              match EConstr.kind sigma (EConstr.of_constr a') with
+              match EConstr.kind sigma a' with
               | Construct cstr ->
                   let l = try Constrmap.find (fst cstr) cstrs with Not_found -> [] in
                   Constrmap.add (fst cstr) ((args,id)::l) cstrs
@@ -691,7 +690,7 @@ let find_projectable_constructor env evd cstr k args cstr_subst =
       List.filter (fun (args',id) ->
         (* is_conv is maybe too strong (and source of useless computation) *)
         (* (at least expansion of aliases is needed) *)
-        Array.for_all2 (fun c1 c2 -> is_conv env evd c1 (EConstr.of_constr c2)) args args') l in
+        Array.for_all2 (fun c1 c2 -> is_conv env evd c1 c2) args args') l in
     List.map snd l
   with Not_found ->
     []
@@ -1104,14 +1103,14 @@ exception CannotProject of evar_map * EConstr.existential
 
 let rec is_constrainable_in top evd k (ev,(fv_rels,fv_ids) as g) t =
   let f,args = decompose_app_vect evd t in
-  match EConstr.kind evd (EConstr.of_constr f) with
+  match EConstr.kind evd f with
   | Construct ((ind,_),u) ->
     let n = Inductiveops.inductive_nparams ind in
     if n > Array.length args then true (* We don't try to be more clever *)
     else
       let params = fst (Array.chop n args) in
-      Array.for_all (EConstr.of_constr %> is_constrainable_in false evd k g) params
-  | Ind _ -> Array.for_all (EConstr.of_constr %> is_constrainable_in false evd k g) args
+      Array.for_all (is_constrainable_in false evd k g) params
+  | Ind _ -> Array.for_all (is_constrainable_in false evd k g) args
   | Prod (na,t1,t2) -> is_constrainable_in false evd k g t1 && is_constrainable_in false evd k g t2
   | Evar (ev',_) -> top || not (Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
   | Var id -> Id.Set.mem id fv_ids
@@ -1463,8 +1462,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
         progress := true;
         match
           let c,args = decompose_app_vect !evdref t in
-          let args = Array.map EConstr.of_constr args in
-          match EConstr.kind !evdref (EConstr.of_constr c) with
+          match EConstr.kind !evdref c with
           | Construct (cstr,u) when noccur_between !evdref 1 k t ->
             (* This is common case when inferring the return clause of match *)
             (* (currently rudimentary: we do not treat the case of multiple *)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index cb8b253232..9c5a2e894a 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -451,13 +451,13 @@ let extract_mrectype sigma t =
   let open EConstr in
   let (t, l) = decompose_app sigma t in
   match EConstr.kind sigma t with
-    | Ind ind -> (ind, List.map EConstr.Unsafe.to_constr l)
+    | Ind ind -> (ind, l)
     | _ -> raise Not_found
 
 let find_mrectype_vect env sigma c =
   let open EConstr in
   let (t, l) = Termops.decompose_app_vect sigma (EConstr.of_constr (whd_all env sigma c)) in
-  match EConstr.kind sigma (EConstr.of_constr t) with
+  match EConstr.kind sigma t with
     | Ind ind -> (ind, l)
     | _ -> raise Not_found
 
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 1614e1817e..4bb4847591 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -161,9 +161,9 @@ val make_arity : env -> bool -> inductive_family -> sorts -> types
 val build_branch_type : env -> bool -> constr -> constructor_summary -> types
 
 (** Raise [Not_found] if not given a valid inductive type *)
-val extract_mrectype : evar_map -> EConstr.t -> pinductive * constr list
-val find_mrectype    : env -> evar_map -> EConstr.types -> pinductive * constr list
-val find_mrectype_vect : env -> evar_map -> EConstr.types -> pinductive * constr array
+val extract_mrectype : evar_map -> EConstr.t -> pinductive * EConstr.constr list
+val find_mrectype    : env -> evar_map -> EConstr.types -> pinductive * EConstr.constr list
+val find_mrectype_vect : env -> evar_map -> EConstr.types -> pinductive * EConstr.constr array
 val find_rectype     : env -> evar_map -> EConstr.types -> inductive_type
 val find_inductive   : env -> evar_map -> EConstr.types -> pinductive * constr list
 val find_coinductive : env -> evar_map -> EConstr.types -> pinductive * constr list
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index c792bf2ca9..f814028f98 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -971,7 +971,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	  let pj = pretype_type empty_valcon env_p evdref lvar p in
 	  let ccl = nf_evar !evdref pj.utj_val in
 	  let pred = it_mkLambda_or_LetIn ccl psign in
-	  let typ = lift (- nar) (EConstr.of_constr (beta_applist !evdref (pred,[cj.uj_val]))) in
+	  let typ = lift (- nar) (beta_applist !evdref (pred,[cj.uj_val])) in
 	    pred, typ
 	| None ->
 	  let p = match tycon with
@@ -987,7 +987,6 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	let n = Context.Rel.length cs.cs_args in
 	let pi = lift n pred in (* liftn n 2 pred ? *)
 	let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in
-	let pi = EConstr.of_constr pi in
 	let csgn =
 	  if not !allow_anonymous_refs then
 	    List.map (set_name Anonymous) cs.cs_args
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 31354217fd..6ec3cd985c 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -669,7 +669,7 @@ let beta_app sigma (c,l) =
 
 let beta_applist sigma (c,l) =
   let zip s = Stack.zip sigma s in
-  EConstr.Unsafe.to_constr (stacklam zip [] sigma c (Stack.append_app_list l Stack.empty))
+  stacklam zip [] sigma c (Stack.append_app_list l Stack.empty)
 
 (* Iota reduction tools *)
 
@@ -1611,8 +1611,8 @@ let meta_reducible_instance evd b =
     let u = whd_betaiota Evd.empty u (** FIXME *) in
     let u = EConstr.of_constr u in
     match EConstr.kind evd u with
-    | Case (ci,p,c,bl) when EConstr.isMeta evd (EConstr.of_constr (strip_outer_cast evd c)) ->
-	let m = destMeta evd (EConstr.of_constr (strip_outer_cast evd c)) in
+    | Case (ci,p,c,bl) when EConstr.isMeta evd (strip_outer_cast evd c) ->
+	let m = destMeta evd (strip_outer_cast evd c) in
 	(match
 	  try
 	    let g, s = Metamap.find m metas in
@@ -1623,8 +1623,8 @@ let meta_reducible_instance evd b =
 	  with
 	    | Some g -> irec (mkCase (ci,p,g,bl))
 	    | None -> mkCase (ci,irec p,c,Array.map irec bl))
-    | App (f,l) when EConstr.isMeta evd (EConstr.of_constr (strip_outer_cast evd f)) ->
-	let m = destMeta evd (EConstr.of_constr (strip_outer_cast evd f)) in
+    | App (f,l) when EConstr.isMeta evd (strip_outer_cast evd f) ->
+	let m = destMeta evd (strip_outer_cast evd f) in
 	(match
 	  try
 	    let g, s = Metamap.find m metas in
@@ -1671,8 +1671,8 @@ let head_unfold_under_prod ts env sigma c =
       | Prod (n,t,c) -> mkProd (n,aux t, aux c)
       | _ ->
 	  let (h,l) = decompose_app_vect sigma c in
-	  match EConstr.kind sigma (EConstr.of_constr h) with
-	    | Const cst -> beta_app sigma (unfold cst, Array.map EConstr.of_constr l)
+	  match EConstr.kind sigma h with
+	    | Const cst -> beta_app sigma (unfold cst, l)
 	    | _ -> c in
   EConstr.Unsafe.to_constr (aux c)
 
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 1e6527b297..3b3242537f 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -204,7 +204,7 @@ val shrink_eta : EConstr.constr -> EConstr.constr
 
 val safe_evar_value : evar_map -> existential -> constr option
 
-val beta_applist : evar_map -> EConstr.t * EConstr.t list -> constr
+val beta_applist : evar_map -> EConstr.t * EConstr.t list -> EConstr.constr
 
 val hnf_prod_app     : env ->  evar_map -> EConstr.t -> EConstr.t -> constr
 val hnf_prod_appvect : env ->  evar_map -> EConstr.t -> EConstr.t array -> constr
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 88899e633e..3142ea5cba 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -59,7 +59,7 @@ let local_def (na, b, t) =
   LocalDef (na, inj b, inj t)
 
 let get_type_from_constraints env sigma t =
-  if isEvar sigma (EConstr.of_constr (fst (decompose_app_vect sigma t))) then
+  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
@@ -102,7 +102,7 @@ let retype ?(polyprop=true) sigma =
   let rec type_of env cstr =
     match EConstr.kind sigma cstr with
     | Meta n ->
-      EConstr.of_constr (try strip_outer_cast sigma (EConstr.of_constr (Evd.meta_ftype sigma n).Evd.rebus)
+      (try strip_outer_cast sigma (EConstr.of_constr (Evd.meta_ftype sigma n).Evd.rebus)
        with Not_found -> retype_error (BadMeta n))
     | Rel n ->
 	let ty = EConstr.of_constr (RelDecl.get_type (lookup_rel n env)) in
@@ -135,10 +135,10 @@ let retype ?(polyprop=true) sigma =
     | CoFix (i,(_,tys,_)) -> tys.(i)
     | App(f,args) when is_template_polymorphic env sigma f ->
 	let t = type_of_global_reference_knowing_parameters env f args in
-        EConstr.of_constr (strip_outer_cast sigma (subst_type env sigma t (Array.to_list args)))
+        strip_outer_cast sigma (subst_type env sigma t (Array.to_list args))
     | App(f,args) ->
-        EConstr.of_constr (strip_outer_cast sigma
-          (subst_type env sigma (type_of env f) (Array.to_list args)))
+        strip_outer_cast sigma
+          (subst_type env sigma (type_of env f) (Array.to_list args))
     | Proj (p,c) ->
        let ty = type_of env c in
        EConstr.of_constr (try
@@ -259,6 +259,5 @@ let expand_projection env sigma pr c args =
     try Inductiveops.find_mrectype env sigma (EConstr.of_constr ty) 
     with Not_found -> retype_error BadRecursiveType
   in
-  let ind_args = List.map EConstr.of_constr ind_args in
     mkApp (mkConstU (Projection.constant pr,u), 
 	   Array.of_list (ind_args @ (c :: args)))
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 1ec8deb1b5..1d179c6834 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -427,8 +427,6 @@ let solve_arity_problem env sigma fxminargs c =
   let rec check strict c =
     let c' = EConstr.of_constr (whd_betaiotazeta sigma c) in
     let (h,rcargs) = decompose_app_vect sigma c' in
-    let rcargs = Array.map EConstr.of_constr rcargs in
-    let h = EConstr.of_constr h in
     match EConstr.kind sigma h with
         Evar(i,_) when Evar.Map.mem i fxminargs && not (Evd.is_defined !evm i) ->
           let minargs = Evar.Map.find i fxminargs in
@@ -734,14 +732,13 @@ and reduce_params env sigma stack l =
 and whd_simpl_stack env sigma =
   let rec redrec s =
     let (x, stack) = decompose_app_vect sigma s in
-    let stack = Array.map_to_list EConstr.of_constr stack in
-    let x = EConstr.of_constr x in
+    let stack = Array.to_list stack in
     let s' = (x, stack) in
     match EConstr.kind sigma x with
       | Lambda (na,t,c) ->
           (match stack with
              | [] -> s'
-             | a :: rest -> redrec (EConstr.of_constr (beta_applist sigma (x, stack))))
+             | a :: rest -> redrec (beta_applist sigma (x, stack)))
       | LetIn (n,b,t,c) -> redrec (applist (Vars.substl [b] c, stack))
       | App (f,cl) -> redrec (applist(f, (Array.to_list cl)@stack))
       | Cast (c,_,_) -> redrec (applist(c, stack))
@@ -1122,14 +1119,12 @@ let fold_one_com com env sigma c =
      unfold produces it, so that the "unfold f; fold f" configuration works
      to refold fix expressions *)
   let a = subst_term sigma (EConstr.of_constr (clos_norm_flags unfold_side_red env sigma rcom)) c in
-  let a = EConstr.of_constr a in
   if not (EConstr.eq_constr sigma a c) then
     Vars.subst1 com a
   else
     (* Then reason on the non beta-iota-zeta form for compatibility -
        even if it is probably a useless configuration *)
     let a = subst_term sigma rcom c in
-    let a = EConstr.of_constr a in
     Vars.subst1 com a
 
 let fold_commands cl env sigma c =
@@ -1195,7 +1190,7 @@ let reduce_to_ind_gen allow_product env sigma t =
   let rec elimrec env t l =
     let t = hnf_constr env sigma t in
     let t = EConstr.of_constr t in
-    match EConstr.kind sigma (EConstr.of_constr (fst (decompose_app_vect sigma t))) with
+    match EConstr.kind sigma (fst (decompose_app_vect sigma t)) with
       | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t l)
       | Prod (n,ty,t') ->
 	  let open Context.Rel.Declaration in
@@ -1208,7 +1203,7 @@ let reduce_to_ind_gen allow_product env sigma t =
 	     was partially the case between V5.10 and V8.1 *)
 	  let t' = whd_all env sigma t in
 	  let t' = EConstr.of_constr t' in
-	  match EConstr.kind sigma (EConstr.of_constr (fst (decompose_app_vect sigma t'))) with
+	  match EConstr.kind sigma (fst (decompose_app_vect sigma t')) with
 	    | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t' l)
 	    | _ -> user_err  (str"Not an inductive product.")
   in
@@ -1275,7 +1270,6 @@ let reduce_to_ref_gen allow_product env sigma ref t =
   (* lazily reduces to match the head of [t] with the expected [ref] *)
   let rec elimrec env t l =
     let c, _ = decompose_app_vect sigma t in
-    let c = EConstr.of_constr c in
     match EConstr.kind sigma c with
       | Prod (n,ty,t') ->
           if allow_product then
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index a970c434f4..f59a6dcd94 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -156,17 +156,17 @@ let class_of_constr sigma c =
   try Some (dest_class_arity (Global.env ()) sigma c)
   with e when CErrors.noncritical e -> None
 
-let is_class_constr c = 
-  try let gr, u = Universes.global_of_constr c in
+let is_class_constr sigma c = 
+  try let gr, u = Termops.global_of_constr sigma c in
 	Refmap.mem gr !classes
   with Not_found -> false
 
 let rec is_class_type evd c =
   let c, _ = Termops.decompose_app_vect evd c in
-    match EConstr.kind evd (EConstr.of_constr c) with
+    match EConstr.kind evd c with
     | Prod (_, _, t) -> is_class_type evd t
     | Cast (t, _, _) -> is_class_type evd t
-    | _ -> is_class_constr c
+    | _ -> is_class_constr evd c
       
 let is_class_evar evd evi =
   is_class_type evd (EConstr.of_constr evi.Evd.evar_concl)
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 29697260f7..40ef2450a3 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -138,7 +138,7 @@ let e_type_case_branches env evdref (ind,largs) pj c =
   let nparams = inductive_params specif in
   let (params,realargs) = List.chop nparams largs in
   let p = pj.uj_val in
-  let realargs = List.map EConstr.of_constr realargs in
+  let params = List.map EConstr.Unsafe.to_constr params in
   let () = e_is_correct_arity env evdref c pj ind specif params in
   let lc = build_branches_type ind specif params (EConstr.to_constr !evdref p) in
   let lc = Array.map EConstr.of_constr lc in
@@ -232,7 +232,6 @@ let judge_of_projection env sigma p cj =
     try find_mrectype env sigma cj.uj_type
     with Not_found -> error_case_not_inductive env sigma cj
   in
-  let args = List.map EConstr.of_constr args in
     let ty = EConstr.of_constr (CVars.subst_instance_constr u pb.Declarations.proj_type) in
     let ty = substl (cj.uj_val :: List.rev args) ty in
       {uj_val = EConstr.mkProj (p,cj.uj_val);
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 81d9ecad50..169dd45bc8 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -632,7 +632,7 @@ let check_compatibility env pbty flags (sigma,metasubst,evarsubst : subst0) tyM
 
 let rec is_neutral env sigma ts t =
   let (f, l) = decompose_app_vect sigma t in
-    match EConstr.kind sigma (EConstr.of_constr f) with
+    match EConstr.kind sigma f with
     | Const (c, u) ->
       not (Environ.evaluable_constant c env) ||
       not (is_transparent env (ConstKey c)) ||
@@ -1488,10 +1488,6 @@ let w_unify_core_0 env evd with_types cv_pb flags m n =
 let w_typed_unify env evd = w_unify_core_0 env evd true
 
 let w_typed_unify_array env evd flags f1 l1 f2 l2 =
-  let f1 = EConstr.of_constr f1 in
-  let f2 = EConstr.of_constr f2 in
-  let l1 = Array.map EConstr.of_constr l1 in
-  let l2 = Array.map EConstr.of_constr l2 in
   let f1,l1,f2,l2 = adjust_app_array_size f1 l1 f2 l2 in
   let (mc1,evd') = retract_coercible_metas evd in
   let fold_subst subst m n = unify_0_with_initial_metas subst true env CONV flags.core_unify_flags  m n in
@@ -1743,7 +1739,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
   let bestexn = ref None in
   let kop = Keys.constr_key (EConstr.to_constr evd op) in
   let rec matchrec cl =
-    let cl = EConstr.of_constr (strip_outer_cast evd cl) in
+    let cl = strip_outer_cast evd cl in
     (try
        if closed0 evd cl && not (isEvar evd cl) && keyed_unify env evd kop cl then
        (try
@@ -1837,7 +1833,6 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) =
   in
   let rec matchrec cl =
     let cl = strip_outer_cast evd cl in
-    let cl = EConstr.of_constr cl in
       (bind
 	  (if closed0 evd cl
 	  then return (fun () -> w_typed_unify env evd CONV flags op cl,cl)
@@ -1898,7 +1893,7 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t =
                unify pre-existing non frozen evars of the goal or of the
                pattern *)
           set_no_delta_flags flags in
-	let t' = (EConstr.of_constr (strip_outer_cast evd op),t) in
+	let t' = (strip_outer_cast evd op,t) in
         let (evd',cl) =
           try
   	    if is_keyed_unification () then
@@ -1992,7 +1987,7 @@ let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 =
   let hd2,l2 = decompose_app_vect evd (EConstr.of_constr (whd_nored evd ty2)) in
   let is_empty1 = Array.is_empty l1 in
   let is_empty2 = Array.is_empty l2 in
-    match kind_of_term hd1, not is_empty1, kind_of_term hd2, not is_empty2 with
+    match EConstr.kind evd hd1, not is_empty1, EConstr.kind evd hd2, not is_empty2 with
       (* Pattern case *)
       | (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true)
 	  when Int.equal (Array.length l1) (Array.length l2) ->