Reductionops now return EConstrs.

20 files changed, 171 insertions, 192 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 76ced2b1d..c0141f011 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1057,7 +1057,6 @@ let specialize_predicate newtomatchs (names,depna) arsign cs tms ccl =
   (* Note: applying the substitution in tms is not important (is it sure?) *)
   let ccl'' =
     whd_betaiota Evd.empty (subst_predicate (realargsi, copti) ccl' tms) in
-  let ccl'' = EConstr.of_constr ccl'' in
   (* We adjust ccl st: gamma, x'1..x'n, x1..xn, tms |- ccl'' *)
   let ccl''' = liftn_predicate n (n+1) ccl'' tms in
   (* We finally get gamma,x'1..x'n,x |- [X1;x1:I(X1)]..[Xn;xn:I(Xn)]pred'''*)
@@ -1065,8 +1064,8 @@ let specialize_predicate newtomatchs (names,depna) arsign cs tms ccl =
 
 let find_predicate loc env evdref p current (IndType (indf,realargs)) dep tms =
   let pred = abstract_predicate env !evdref indf current realargs dep tms p in
-  (pred, EConstr.of_constr (whd_betaiota !evdref
-           (applist (pred, realargs@[current]))))
+  (pred, whd_betaiota !evdref
+           (applist (pred, realargs@[current])))
 
 (* Take into account that a type has been discovered to be inductive, leading
    to more dependencies in the predicate if the type has indices *)
@@ -1221,7 +1220,7 @@ let rec generalize_problem names pb = function
       | LocalDef (Anonymous,_,_) -> pb', deps
       | _ ->
 	 (* for better rendering *)
-	let d = RelDecl.map_type (fun c -> whd_betaiota !(pb.evdref) (EConstr.of_constr c)) d in
+	let d = RelDecl.map_type (fun c -> EConstr.Unsafe.to_constr (whd_betaiota !(pb.evdref) (EConstr.of_constr c))) d in
         let tomatch = lift_tomatch_stack 1 pb'.tomatch in
         let tomatch = relocate_index_tomatch !(pb.evdref) (i+1) 1 tomatch in
         { pb' with
@@ -1400,7 +1399,6 @@ and match_current pb (initial,tomatch) =
 	      pred current indt (names,dep) tomatch in
 	  let ci = make_case_info pb.env (fst mind) pb.casestyle in
 	  let pred = nf_betaiota !(pb.evdref) pred in
-	  let pred = EConstr.of_constr pred in
 	  let case =
 	    make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals
 	  in
@@ -1638,7 +1636,6 @@ let rec list_assoc_in_triple x = function
 
 let abstract_tycon loc env evdref subst tycon extenv t =
   let t = nf_betaiota !evdref t in (* it helps in some cases to remove K-redex*)
-  let t = EConstr.of_constr t in
   let src = match EConstr.kind !evdref t with
     | Evar (evk,_) -> (loc,Evar_kinds.SubEvar evk)
     | _ -> (loc,Evar_kinds.CasesType true) in
@@ -1734,7 +1731,7 @@ let build_inversion_problem loc env sigma tms t =
     let id = next_name_away (named_hd env (EConstr.Unsafe.to_constr t) Anonymous) avoid in
     PatVar (Loc.ghost,Name id), ((id,t)::subst, id::avoid) in
   let rec reveal_pattern t (subst,avoid as acc) =
-    match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with
+    match EConstr.kind sigma (whd_all env sigma t) with
     | Construct (cstr,u) -> PatCstr (Loc.ghost,cstr,[],Anonymous), acc
     | App (f,v) when isConstruct sigma f ->
 	let cstr,u = destConstruct sigma f in
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 23d20dad3..e4331aade 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -234,7 +234,6 @@ let class_of env sigma t =
       (t, n1, i, u, args)
     with Not_found ->
       let t = Tacred.hnf_constr env sigma t in
-      let t = EConstr.of_constr t in
       let (cl, u, args) = find_class_type sigma t in
       let (i, { cl_param = n1 } ) = class_info cl in
       (t, n1, i, u, args)
@@ -279,7 +278,6 @@ let apply_on_class_of env sigma t cont =
   with Not_found ->
     (* Is it worth to be more incremental on the delta steps? *)
     let t = Tacred.hnf_constr env sigma t in
-    let t = EConstr.of_constr t in
     let (cl, u, args) = find_class_type sigma t in
     let (i, { cl_param = n1 } ) = class_info cl in
     if not (Int.equal (List.length args) n1) then raise Not_found;
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 48f7be4bb..7e8559630 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -64,7 +64,7 @@ let apply_coercion_args env evd check isproj argl funj =
 	{ uj_val = applist (j_val funj,argl);
 	  uj_type = typ }
     | h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *)
-      match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref typ)) with
+      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
 	  raise NoCoercion;
@@ -96,7 +96,7 @@ let make_existential loc ?(opaque = not (get_proofs_transparency ()))  env evdre
   Evarutil.e_new_evar env evdref ~src c
 
 let app_opt env evdref f t =
-  EConstr.of_constr (whd_betaiota !evdref (app_opt f t))
+  whd_betaiota !evdref (app_opt f t)
 
 let pair_of_array a = (a.(0), a.(1))
 
@@ -134,11 +134,10 @@ let local_assum (na, t) =
 let mu env evdref t =
   let rec aux v =
     let v' = hnf env !evdref v in
-    let v' = EConstr.of_constr v' in
       match disc_subset !evdref v' with
       | Some (u, p) ->
 	let f, ct = aux u in
-	let p = EConstr.of_constr (hnf_nodelta env !evdref p) in
+	let p = hnf_nodelta env !evdref p in
 	  (Some (fun x ->
 		   app_opt env evdref 
 		     f (papp evdref sig_proj1 [| u; p; x |])),
@@ -152,8 +151,6 @@ and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr)
   let open Context.Rel.Declaration in
   let rec coerce_unify env x y =
     let x = hnf env !evdref x and y = hnf env !evdref y in
-    let x = EConstr.of_constr x in
-    let y = EConstr.of_constr y in
       try
 	evdref := the_conv_x_leq env x y !evdref;
 	None
@@ -162,7 +159,7 @@ and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr)
     let subco () = subset_coerce env evdref x y in
     let dest_prod c =
       match Reductionops.splay_prod_n env (!evdref) 1 c with
-      | [LocalAssum (na,t) | LocalDef (na,_,t)], c -> (na, EConstr.of_constr t), EConstr.of_constr c
+      | [LocalAssum (na,t) | LocalDef (na,_,t)], c -> (na, EConstr.of_constr t), c
       | _ -> raise NoSubtacCoercion
     in
     let coerce_application typ typ' c c' l l' =
@@ -344,7 +341,7 @@ let app_coercion env evdref coercion v =
   | None -> v
   | Some f ->
      let v' = Typing.e_solve_evars env evdref (f v) in
-     EConstr.of_constr (whd_betaiota !evdref (EConstr.of_constr v'))
+     whd_betaiota !evdref (EConstr.of_constr v')
 
 let coerce_itf loc env evd v t c1 =
   let evdref = ref evd in
@@ -381,7 +378,6 @@ let apply_coercion env sigma p hj typ_cl =
 (* Try to coerce to a funclass; raise NoCoercion if not possible *)
 let inh_app_fun_core env evd j =
   let t = whd_all env evd j.uj_type in
-  let t = EConstr.of_constr t in
     match EConstr.kind evd t with
     | Prod (_,_,_) -> (evd,j)
     | Evar ev ->
@@ -413,7 +409,7 @@ let inh_app_fun resolve_tc env evd j =
     with NoCoercion -> (evd, j)
 
 let type_judgment env sigma j =
-  match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma j.uj_type)) with
+  match EConstr.kind sigma (whd_all env sigma j.uj_type) with
     | Sort s -> {utj_val = j.uj_val; utj_type = s }
     | _ -> error_not_a_type env sigma j
 
@@ -429,7 +425,7 @@ let inh_tosort_force loc env evd j =
 
 let inh_coerce_to_sort loc env evd j =
   let typ = whd_all env evd j.uj_type in
-    match EConstr.kind evd (EConstr.of_constr typ) with
+    match EConstr.kind evd typ with
     | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s })
     | Evar ev ->
 	let (evd',s) = Evardefine.define_evar_as_sort env evd ev in
@@ -480,8 +476,8 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
     try inh_coerce_to_fail env evd rigidonly v t c1
     with NoCoercion ->
       match
-      EConstr.kind evd (EConstr.of_constr (whd_all env evd t)),
-      EConstr.kind evd (EConstr.of_constr (whd_all env evd c1))
+      EConstr.kind evd (whd_all env evd t),
+      EConstr.kind evd (whd_all env evd c1)
       with
       | Prod (name,t1,t2), Prod (_,u1,u2) ->
           (* Conversion did not work, we may succeed with a coercion. *)
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index 3babc48a7..d4b46c046 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -39,7 +39,7 @@ let env_nf_evar sigma env =
 let env_nf_betaiotaevar sigma env =
   process_rel_context
     (fun d e ->
-      push_rel (RelDecl.map_constr (fun c -> Reductionops.nf_betaiota sigma (EConstr.of_constr c)) d) e) env
+      push_rel (RelDecl.map_constr (fun c -> EConstr.Unsafe.to_constr (Reductionops.nf_betaiota sigma (EConstr.of_constr c))) d) e) env
 
 (****************************************)
 (* Operations on value/type constraints *)
@@ -85,7 +85,6 @@ let define_pure_evar_as_product evd evk =
   let evenv = evar_env evi in
   let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in
   let concl = Reductionops.whd_all evenv evd (EConstr.of_constr evi.evar_concl) in
-  let concl = EConstr.of_constr concl in
   let s = destSort evd concl in
   let evd1,(dom,u1) =
     let evd = Sigma.Unsafe.of_evar_map evd in
@@ -138,7 +137,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 = EConstr.of_constr (Reductionops.whd_all evenv evd (EConstr.of_constr (evar_concl evi))) in
+  let typ = Reductionops.whd_all evenv evd (EConstr.of_constr (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
@@ -177,7 +176,6 @@ let define_evar_as_sort env evd (ev,args) =
   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 = EConstr.of_constr concl in
   let sort = destSort evd concl in
   let evd' = Evd.define ev (Constr.mkSort s) evd in
   Evd.set_leq_sort env evd' (Type (Univ.super u)) sort, s
@@ -190,7 +188,7 @@ let define_evar_as_sort env evd (ev,args) =
 let split_tycon loc env evd tycon =
   let rec real_split evd c =
     let t = Reductionops.whd_all env evd c in
-      match EConstr.kind evd (EConstr.of_constr t) with
+      match EConstr.kind evd t with
 	| Prod (na,dom,rng) -> evd, (na, dom, rng)
 	| Evar ev (* ev is undefined because of whd_all *) ->
 	    let (evd',prod) = define_evar_as_product evd ev in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 65b6d287d..27436fdd8 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -149,7 +149,7 @@ let recheck_applications conv_algo env evdref t =
        let argsty = Array.map (fun x -> aux env x; EConstr.of_constr (Retyping.get_type_of env !evdref x)) args in
        let rec aux i ty =
 	 if i < Array.length argsty then
-	 match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref ty)) with
+	 match EConstr.kind !evdref (whd_all env !evdref ty) with
 	 | Prod (na, dom, codom) ->
 	    (match conv_algo env !evdref Reduction.CUMUL argsty.(i) dom with
 	     | Success evd -> evdref := evd;
@@ -814,7 +814,7 @@ let rec do_projection_effects define_fun env ty evd = function
       let evd = Evd.define evk (Constr.mkVar id) evd in
       (* TODO: simplify constraints involving evk *)
       let evd = do_projection_effects define_fun env ty evd p in
-      let ty = EConstr.of_constr (whd_all env evd (Lazy.force ty)) in
+      let ty = whd_all env evd (Lazy.force ty) in
       if not (isSort evd ty) then
         (* Don't try to instantiate if a sort because if evar_concl is an
            evar it may commit to a univ level which is not the right
@@ -1494,7 +1494,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
           map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1)
 					imitate envk t
   in
-  let rhs = EConstr.of_constr (whd_beta evd rhs) (* heuristic *) in
+  let rhs = whd_beta evd rhs (* heuristic *) in
   let fast rhs = 
     let filter_ctxt = evar_filtered_context evi in
     let names = ref Idset.empty in
@@ -1576,7 +1576,7 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
         raise e
     | OccurCheckIn (evd,rhs) ->
         (* last chance: rhs actually reduces to ev *)
-        let c = EConstr.of_constr (whd_all env evd rhs) in
+        let c = whd_all env evd rhs in
         match EConstr.kind evd c with
         | Evar (evk',argsv2) when Evar.equal evk evk' ->
 	    solve_refl (fun env sigma pb c c' -> is_fconv pb env sigma c c')
@@ -1637,7 +1637,7 @@ let reconsider_conv_pbs conv_algo evd =
 (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
 let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) =
   try
-    let t2 = EConstr.of_constr (whd_betaiota evd t2) in (* includes whd_evar *)
+    let t2 = whd_betaiota evd t2 in (* includes whd_evar *)
     let evd = evar_define conv_algo ~choose env evd pbty ev1 t2 in
       reconsider_conv_pbs conv_algo evd
   with
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 4fa5ad06d..1adeb4db2 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -173,6 +173,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
 	      base
       	| _ ->
 	   let t' = whd_all env sigma (EConstr.of_constr p) in
+	   let t' = EConstr.Unsafe.to_constr t' in
 	   if Term.eq_constr p' t' then assert false
 	   else prec env i sign t'
     in
@@ -247,6 +248,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
             applist(lift i fk,realargs@[arg])
      	| _ ->
 	   let t' = whd_all env sigma (EConstr.of_constr p) in
+	   let t' = EConstr.Unsafe.to_constr t' in
 	     if Term.eq_constr t' p' then assert false
 	     else prec env i hyps t'
     in
@@ -265,7 +267,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
            | None ->
 	       mkLambda_name env
 		 (n,t,process_constr (push_rel d env) (i+1)
-		    (whd_beta Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1)]))))
+		    (EConstr.Unsafe.to_constr (whd_beta Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1)])))))
 		    (cprest,rest))
            | Some(_,f_0) ->
 	       let nF = lift (i+1+decF) f_0 in
@@ -273,7 +275,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
 	       let arg = process_pos env' nF (lift 1 t) in
                mkLambda_name env
 		 (n,t,process_constr env' (i+1)
-		    (whd_beta Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1); arg]))))
+		    (EConstr.Unsafe.to_constr (whd_beta Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1); arg])))))
 		    (cprest,rest)))
     | (LocalDef (n,c,t) as d)::cprest, rest ->
 	mkLetIn
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 9c5a2e894..120adb9fe 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -456,7 +456,7 @@ let extract_mrectype sigma t =
 
 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
+  let (t, l) = Termops.decompose_app_vect sigma (whd_all env sigma c) in
   match EConstr.kind sigma t with
     | Ind ind -> (ind, l)
     | _ -> raise Not_found
@@ -466,7 +466,7 @@ let find_mrectype env sigma c =
 
 let find_rectype env sigma c =
   let open EConstr in
-  let (t, l) = decompose_app sigma (EConstr.of_constr (whd_all env sigma c)) in
+  let (t, l) = decompose_app sigma (whd_all env sigma c) in
   match EConstr.kind sigma t with
     | Ind (ind,u as indu) ->
         let (mib,mip) = Inductive.lookup_mind_specif env ind in
@@ -478,7 +478,7 @@ let find_rectype env sigma c =
 
 let find_inductive env sigma c =
   let open EConstr in
-  let (t, l) = decompose_app sigma (EConstr.of_constr (whd_all env sigma c)) in
+  let (t, l) = decompose_app sigma (whd_all env sigma c) in
   match EConstr.kind sigma t with
     | Ind ind
         when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> Decl_kinds.CoFinite ->
@@ -488,7 +488,7 @@ let find_inductive env sigma c =
 
 let find_coinductive env sigma c =
   let open EConstr in
-  let (t, l) = decompose_app sigma (EConstr.of_constr (whd_all env sigma c)) in
+  let (t, l) = decompose_app sigma (whd_all env sigma c) in
   match EConstr.kind sigma t with
     | Ind ind
         when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == Decl_kinds.CoFinite ->
@@ -503,7 +503,7 @@ let find_coinductive env sigma c =
 
 let is_predicate_explicitly_dep env sigma pred arsign =
   let rec srec env pval arsign =
-    let pv' = EConstr.of_constr (whd_all env sigma pval) in
+    let pv' = whd_all env sigma pval in
     match EConstr.kind sigma pv', arsign with
       | Lambda (na,t,b), (LocalAssum _)::arsign ->
 	  srec (push_rel_assum (na, t) env) b arsign
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index cdaa4e9ee..0228f63cd 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -404,7 +404,7 @@ let native_norm env sigma c ty =
         let t2 = Sys.time () in
         let time_info = Format.sprintf "Reification done in %.5f@." (t2 -. t1) in
         if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
-        res
+        EConstr.of_constr res
     | _ -> anomaly (Pp.str "Compilation failure") 
 
 let native_conv_generic pb sigma t =
diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli
index ba46138a4..c899340c8 100644
--- a/pretyping/nativenorm.mli
+++ b/pretyping/nativenorm.mli
@@ -12,7 +12,7 @@ open Evd
 
 (** This module implements normalization by evaluation to OCaml code *)
 
-val native_norm : env -> evar_map -> constr -> types -> Constr.t
+val native_norm : env -> evar_map -> constr -> types -> constr
 
 (** Conversion with inference of universe constraints *)
 val native_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f814028f9..7d2c96bb9 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -743,7 +743,6 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	let argloc = loc_of_glob_constr c in
 	let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env.ExtraEnv.env) evdref resj in
         let resty = whd_all env.ExtraEnv.env !evdref resj.uj_type in
-        let resty = EConstr.of_constr resty in
       	  match EConstr.kind !evdref resty with
 	  | Prod (na,c1,c2) ->
 	    let tycon = Some c1 in
@@ -917,7 +916,6 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	      @[EConstr.of_constr (build_dependent_constructor cs)] in
 	    let lp = lift cs.cs_nargs p in
 	    let fty = hnf_lam_applist env.ExtraEnv.env !evdref lp inst in
-	    let fty = EConstr.of_constr fty in
 	    let fj = pretype (mk_tycon fty) env_f evdref lvar d in
 	    let v =
 	      let ind,_ = dest_ind_family indf in
@@ -1100,7 +1098,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
 	     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 (EConstr.of_constr (whd_all env.ExtraEnv.env sigma t)) with
+	       match EConstr.kind sigma (whd_all env.ExtraEnv.env sigma t) with
                | Sort s -> s
                | Evar ev when is_Type (existential_type sigma ev) ->
 		   evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 3230f92da..8362a2a26 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -324,15 +324,15 @@ let lookup_canonical_conversion (proj,pat) =
   assoc_pat pat (Refmap.find proj !object_table)
 
 let is_open_canonical_projection env sigma (c,args) =
+  let open EConstr in
   try
-    let c = EConstr.Unsafe.to_constr c in
-    let ref = global_of_constr c in
+    let (ref, _) = Termops.global_of_constr sigma c in
     let n = find_projection_nparams ref in
     (** Check if there is some canonical projection attached to this structure *)
     let _ = Refmap.find ref !object_table in
     try
       let arg = whd_all env sigma (Stack.nth args n) in
-      let hd = match kind_of_term arg with App (hd, _) -> hd | _ -> arg in
-      not (isConstruct hd)
+      let hd = match EConstr.kind sigma arg with App (hd, _) -> hd | _ -> arg in
+      not (isConstruct sigma hd)
     with Failure _ -> false
   with Not_found -> false
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 6ec3cd985..45e7abcb7 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -588,10 +588,10 @@ end
 (** The type of (machine) states (= lambda-bar-calculus' cuts) *)
 type state = constr * constr Stack.t
 
-type contextual_reduction_function = env -> evar_map -> constr -> Constr.constr
+type contextual_reduction_function = env -> evar_map -> constr -> constr
 type reduction_function = contextual_reduction_function
-type local_reduction_function = evar_map -> constr -> Constr.constr
-type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (Constr.constr, 'r) Sigma.sigma }
+type local_reduction_function = evar_map -> constr -> constr
+type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma }
 
 type contextual_stack_reduction_function =
     env -> evar_map -> constr -> constr * constr list
@@ -629,19 +629,18 @@ let safe_meta_value sigma ev =
 
 let strong whdfun env sigma t =
   let rec strongrec env t =
-    let t = EConstr.of_constr (whdfun env sigma t) in
-    map_constr_with_full_binders sigma push_rel strongrec env t in
-  EConstr.Unsafe.to_constr (strongrec env t)
+    map_constr_with_full_binders sigma push_rel strongrec env (whdfun env sigma t) in
+  strongrec env t
 
 let local_strong whdfun sigma =
-  let rec strongrec t = EConstr.map sigma strongrec (EConstr.of_constr (whdfun sigma t)) in
-  fun c -> EConstr.Unsafe.to_constr (strongrec c)
+  let rec strongrec t = EConstr.map sigma strongrec (whdfun sigma t) in
+  strongrec
 
 let rec strong_prodspine redfun sigma c =
-  let x = EConstr.of_constr (redfun sigma c) in
+  let x = redfun sigma c in
   match EConstr.kind sigma x with
-    | Prod (na,a,b) -> EConstr.Unsafe.to_constr (mkProd (na,a,EConstr.of_constr (strong_prodspine redfun sigma b)))
-    | _ -> EConstr.Unsafe.to_constr x
+    | Prod (na,a,b) -> mkProd (na,a,strong_prodspine redfun sigma b)
+    | _ -> x
 
 (*************************************)
 (*** Reduction using bindingss ***)
@@ -1140,7 +1139,7 @@ let iterate_whd_gen refold flags env sigma s =
   in aux s
 
 let red_of_state_red f sigma x =
-  EConstr.Unsafe.to_constr (Stack.zip sigma (f sigma (x,Stack.empty)))
+  Stack.zip sigma (f sigma (x,Stack.empty))
 
 (* 0. No Reduction Functions *)
 
@@ -1217,9 +1216,9 @@ let nf_evar = Evarutil.nf_evar
 let clos_norm_flags flgs env sigma t =
   try
     let evars ev = safe_evar_value sigma ev in
-    CClosure.norm_val
+    EConstr.of_constr (CClosure.norm_val
       (CClosure.create_clos_infos ~evars flgs env)
-      (CClosure.inject (EConstr.Unsafe.to_constr t))
+      (CClosure.inject (EConstr.Unsafe.to_constr t)))
   with e when is_anomaly e -> error "Tried to normalize ill-typed term"
 
 let nf_beta = clos_norm_flags CClosure.beta (Global.env ())
@@ -1309,6 +1308,7 @@ let sigma_univ_state =
 
 let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
     ?(ts=full_transparent_state) env sigma x y =
+  (** FIXME *)
   let x = EConstr.Unsafe.to_constr x in
   let y = EConstr.Unsafe.to_constr y in
   try
@@ -1352,8 +1352,8 @@ let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 =
 (********************************************************************)
 
 let whd_meta sigma c = match EConstr.kind sigma c with
-  | Meta p -> (try meta_value sigma p with Not_found -> EConstr.Unsafe.to_constr c)
-  | _ -> EConstr.Unsafe.to_constr c
+  | Meta p -> (try EConstr.of_constr (meta_value sigma p) with Not_found -> c)
+  | _ -> c
 
 let default_plain_instance_ident = Id.of_string "H"
 
@@ -1431,26 +1431,26 @@ let instance sigma s c =
  * error message. *)
 
 let hnf_prod_app env sigma t n =
-  match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with
-    | Prod (_,_,b) -> EConstr.Unsafe.to_constr (subst1 n b)
+  match EConstr.kind sigma (whd_all env sigma t) with
+    | Prod (_,_,b) -> subst1 n b
     | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product")
 
 let hnf_prod_appvect env sigma t nl =
-  Array.fold_left (fun acc t -> hnf_prod_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl
+  Array.fold_left (fun acc t -> hnf_prod_app env sigma acc t) t nl
 
 let hnf_prod_applist env sigma t nl =
-  List.fold_left (fun acc t -> hnf_prod_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl
+  List.fold_left (fun acc t -> hnf_prod_app env sigma acc t) t nl
 
 let hnf_lam_app env sigma t n =
-  match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with
-    | Lambda (_,_,b) -> EConstr.Unsafe.to_constr (subst1 n b)
+  match EConstr.kind sigma (whd_all env sigma t) with
+    | Lambda (_,_,b) -> subst1 n b
     | _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction")
 
 let hnf_lam_appvect env sigma t nl =
-  Array.fold_left (fun acc t -> hnf_lam_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl
+  Array.fold_left (fun acc t -> hnf_lam_app env sigma acc t) t nl
 
 let hnf_lam_applist env sigma t nl =
-  List.fold_left (fun acc t -> hnf_lam_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl
+  List.fold_left (fun acc t -> hnf_lam_app env sigma acc t) t nl
 
 let bind_assum (na, t) =
   (na, t)
@@ -1458,7 +1458,6 @@ let bind_assum (na, t) =
 let splay_prod env sigma =
   let rec decrec env m c =
     let t = whd_all env sigma c in
-    let t = EConstr.of_constr t in
     match EConstr.kind sigma t with
       | Prod (n,a,c0) ->
 	  decrec (push_rel (local_assum (n,a)) env)
@@ -1470,7 +1469,6 @@ let splay_prod env sigma =
 let splay_lam env sigma =
   let rec decrec env m c =
     let t = whd_all env sigma c in
-    let t = EConstr.of_constr t in
     match EConstr.kind sigma t with
       | Lambda (n,a,c0) ->
 	  decrec (push_rel (local_assum (n,a)) env)
@@ -1482,7 +1480,7 @@ let splay_lam env sigma =
 let splay_prod_assum env sigma =
   let rec prodec_rec env l c =
     let t = whd_allnolet env sigma c in
-    match EConstr.kind sigma (EConstr.of_constr t) with
+    match EConstr.kind sigma t with
     | Prod (x,t,c)  ->
 	prodec_rec (push_rel (local_assum (x,t)) env)
 	  (Context.Rel.add (local_assum (x,t)) l) c
@@ -1491,9 +1489,9 @@ let splay_prod_assum env sigma =
 	  (Context.Rel.add (local_def (x,b,t)) l) c
     | Cast (c,_,_)    -> prodec_rec env l c
     | _               -> 
-      let t' = whd_all env sigma (EConstr.of_constr t) in
-	if Term.eq_constr t t' then l,t
-	else prodec_rec env l (EConstr.of_constr t')
+      let t' = whd_all env sigma t in
+	if EConstr.eq_constr sigma t t' then l,t
+	else prodec_rec env l t'
   in
   prodec_rec env Context.Rel.empty
 
@@ -1506,8 +1504,8 @@ let splay_arity env sigma c =
 let sort_of_arity env sigma c = snd (splay_arity env sigma c)
 
 let splay_prod_n env sigma n =
-  let rec decrec env m ln c = if Int.equal m 0 then (ln, EConstr.Unsafe.to_constr c) else
-    match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma c)) with
+  let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else
+    match EConstr.kind sigma (whd_all env sigma c) with
       | Prod (n,a,c0) ->
 	  decrec (push_rel (local_assum (n,a)) env)
 	    (m-1) (Context.Rel.add (local_assum (n,a)) ln) c0
@@ -1516,8 +1514,8 @@ let splay_prod_n env sigma n =
   decrec env n Context.Rel.empty
 
 let splay_lam_n env sigma n =
-  let rec decrec env m ln c = if Int.equal m 0 then (ln, EConstr.Unsafe.to_constr c) else
-    match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma c)) with
+  let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else
+    match EConstr.kind sigma (whd_all env sigma c) with
       | Lambda (n,a,c0) ->
 	  decrec (push_rel (local_assum (n,a)) env)
 	    (m-1) (Context.Rel.add (local_assum (n,a)) ln) c0
@@ -1526,7 +1524,7 @@ let splay_lam_n env sigma n =
   decrec env n Context.Rel.empty
 
 let is_sort env sigma t =
-  match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with
+  match EConstr.kind sigma (whd_all env sigma t) with
   | Sort s -> true
   | _ -> false
 
@@ -1559,7 +1557,7 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
 let find_conclusion env sigma =
   let rec decrec env c =
     let t = whd_all env sigma c in
-    match EConstr.kind sigma (EConstr.of_constr t) with
+    match EConstr.kind sigma t with
       | Prod (x,t,c0) -> decrec (push_rel (local_assum (x,t)) env) c0
       | Lambda (x,t,c0) -> decrec (push_rel (local_assum (x,t)) env) c0
       | t -> t
@@ -1579,7 +1577,7 @@ let meta_value evd mv =
     match meta_opt_fvalue evd mv with
     | Some (b,_) ->
       let metas = Metamap.bind valrec b.freemetas in
-      EConstr.of_constr (instance evd metas (EConstr.of_constr b.rebus))
+      instance evd metas (EConstr.of_constr b.rebus)
     | None -> mkMeta mv
   in
   valrec mv
@@ -1589,7 +1587,7 @@ let meta_instance sigma b =
   if Metaset.is_empty fm then b.rebus
   else
     let c_sigma = Metamap.bind (fun mv -> meta_value sigma mv) fm in
-    EConstr.of_constr (instance sigma c_sigma b.rebus)
+    instance sigma c_sigma b.rebus
 
 let nf_meta sigma c =
   let c = EConstr.Unsafe.to_constr c in
@@ -1609,7 +1607,6 @@ let meta_reducible_instance evd b =
   let metas = Metaset.fold fold fm Metamap.empty in
   let rec irec u =
     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 (strip_outer_cast evd c) ->
 	let m = destMeta evd (strip_outer_cast evd c) in
@@ -1674,7 +1671,7 @@ let head_unfold_under_prod ts env sigma c =
 	  match EConstr.kind sigma h with
 	    | Const cst -> beta_app sigma (unfold cst, l)
 	    | _ -> c in
-  EConstr.Unsafe.to_constr (aux c)
+  aux c
 
 let betazetaevar_applist sigma n c l =
   let rec stacklam n env t stack =
@@ -1684,4 +1681,4 @@ let betazetaevar_applist sigma n c l =
     | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack
     | Evar _, _ -> applist (substl env t, stack)
     | _ -> anomaly (Pp.str "Not enough lambda/let's") in
-  EConstr.Unsafe.to_constr (stacklam n [] c l)
+  stacklam n [] c l
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 3b3242537..add1d186b 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Term
+open EConstr
 open Univ
 open Evd
 open Environ
@@ -38,7 +39,6 @@ val set_refolding_in_reduction : bool -> unit
     cst applied to params must convertible to term of the state applied to args
 *)
 module Cst_stack : sig
-  open EConstr
   type t
   val empty : t
   val add_param : constr -> t -> t
@@ -52,7 +52,6 @@ end
 
 
 module Stack : sig
-  open EConstr
   type 'a app_node
 
   val pr_app_node : ('a -> Pp.std_ppcmds) -> 'a app_node -> Pp.std_ppcmds
@@ -109,19 +108,19 @@ end
 
 (************************************************************************)
 
-type state = EConstr.t * EConstr.t Stack.t
+type state = constr * constr Stack.t
 
-type contextual_reduction_function = env -> evar_map -> EConstr.t -> constr
+type contextual_reduction_function = env -> evar_map -> constr -> constr
 type reduction_function = contextual_reduction_function
-type local_reduction_function = evar_map -> EConstr.t -> constr
+type local_reduction_function = evar_map -> constr -> constr
 
-type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> EConstr.t -> (constr, 'r) Sigma.sigma }
+type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma }
 
 type contextual_stack_reduction_function =
-    env -> evar_map -> EConstr.t -> EConstr.t * EConstr.t list
+    env -> evar_map -> constr -> constr * constr list
 type stack_reduction_function = contextual_stack_reduction_function
 type local_stack_reduction_function =
-    evar_map -> EConstr.t -> EConstr.t * EConstr.t list
+    evar_map -> constr -> constr * constr list
 
 type contextual_state_reduction_function =
     env -> evar_map -> state -> state
@@ -139,13 +138,13 @@ val strong_prodspine : local_reduction_function -> local_reduction_function
 val stack_reduction_of_reduction :
   'a reduction_function -> 'a state_reduction_function
 i*)
-val stacklam : (state -> 'a) -> EConstr.t list -> evar_map -> EConstr.t -> EConstr.t Stack.t -> 'a
+val stacklam : (state -> 'a) -> constr list -> evar_map -> constr -> constr Stack.t -> 'a
 
 val whd_state_gen : ?csts:Cst_stack.t -> refold:bool -> tactic_mode:bool ->
   CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state * Cst_stack.t
 
 val iterate_whd_gen : bool -> CClosure.RedFlags.reds ->
-  Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr
+  Environ.env -> Evd.evar_map -> constr -> constr
 
 (** {6 Generic Optimized Reduction Function using Closures } *)
 
@@ -156,11 +155,11 @@ val nf_beta : local_reduction_function
 val nf_betaiota : local_reduction_function
 val nf_betaiotazeta : local_reduction_function
 val nf_all : reduction_function
-val nf_evar : evar_map -> constr -> constr
+val nf_evar : evar_map -> Constr.constr -> Constr.constr
 
 (** Lazy strategy, weak head reduction *)
 
-val whd_evar :  evar_map -> constr -> constr
+val whd_evar :  evar_map -> Constr.constr -> Constr.constr
 val whd_nored : local_reduction_function
 val whd_beta : local_reduction_function
 val whd_betaiota : local_reduction_function
@@ -198,45 +197,45 @@ val whd_zeta_stack : local_stack_reduction_function
 val whd_zeta_state : local_state_reduction_function
 val whd_zeta : local_reduction_function
 
-val shrink_eta : EConstr.constr -> EConstr.constr
+val shrink_eta : constr -> constr
 
 (** Various reduction functions *)
 
-val safe_evar_value : evar_map -> existential -> constr option
+val safe_evar_value : evar_map -> Constr.existential -> Constr.constr option
 
-val beta_applist : evar_map -> EConstr.t * EConstr.t list -> EConstr.constr
+val beta_applist : evar_map -> constr * constr list -> 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
-val hnf_prod_applist : env ->  evar_map -> EConstr.t -> EConstr.t list -> constr
-val hnf_lam_app      : env ->  evar_map -> EConstr.t -> EConstr.t -> constr
-val hnf_lam_appvect  : env ->  evar_map -> EConstr.t -> EConstr.t array -> constr
-val hnf_lam_applist  : env ->  evar_map -> EConstr.t -> EConstr.t list -> constr
+val hnf_prod_app     : env ->  evar_map -> constr -> constr -> constr
+val hnf_prod_appvect : env ->  evar_map -> constr -> constr array -> constr
+val hnf_prod_applist : env ->  evar_map -> constr -> constr list -> constr
+val hnf_lam_app      : env ->  evar_map -> constr -> constr -> constr
+val hnf_lam_appvect  : env ->  evar_map -> constr -> constr array -> constr
+val hnf_lam_applist  : env ->  evar_map -> constr -> constr list -> constr
 
-val splay_prod : env ->  evar_map -> EConstr.t -> (Name.t * EConstr.constr) list * EConstr.constr
-val splay_lam : env ->  evar_map -> EConstr.t -> (Name.t * EConstr.constr) list * EConstr.constr
-val splay_arity : env ->  evar_map -> EConstr.t -> (Name.t * EConstr.constr) list * sorts
-val sort_of_arity : env -> evar_map -> EConstr.t -> sorts
-val splay_prod_n : env ->  evar_map -> int -> EConstr.t -> Context.Rel.t * constr
-val splay_lam_n : env ->  evar_map -> int -> EConstr.t -> Context.Rel.t * constr
+val splay_prod : env ->  evar_map -> constr -> (Name.t * constr) list * constr
+val splay_lam : env ->  evar_map -> constr -> (Name.t * constr) list * constr
+val splay_arity : env ->  evar_map -> constr -> (Name.t * constr) list * sorts
+val sort_of_arity : env -> evar_map -> constr -> sorts
+val splay_prod_n : env ->  evar_map -> int -> constr -> Context.Rel.t * constr
+val splay_lam_n : env ->  evar_map -> int -> constr -> Context.Rel.t * constr
 val splay_prod_assum :
-  env ->  evar_map -> EConstr.t -> Context.Rel.t * constr
+  env ->  evar_map -> constr -> Context.Rel.t * constr
 
 type 'a miota_args = {
-  mP      : EConstr.t;     (** the result type *)
-  mconstr : EConstr.t;     (** the constructor *)
+  mP      : constr;     (** the result type *)
+  mconstr : constr;     (** the constructor *)
   mci     : case_info;  (** special info to re-build pattern *)
   mcargs  : 'a list;    (** the constructor's arguments *)
   mlf     : 'a array }  (** the branch code vector *)
 
-val reducible_mind_case : evar_map -> EConstr.t -> bool
-val reduce_mind_case : evar_map -> EConstr.t miota_args -> EConstr.t
+val reducible_mind_case : evar_map -> constr -> bool
+val reduce_mind_case : evar_map -> constr miota_args -> constr
 
-val find_conclusion : env -> evar_map -> EConstr.t -> (EConstr.t,EConstr.t) kind_of_term
-val is_arity : env ->  evar_map -> EConstr.t -> bool
-val is_sort : env -> evar_map -> EConstr.types -> bool
+val find_conclusion : env -> evar_map -> constr -> (constr,constr) kind_of_term
+val is_arity : env ->  evar_map -> constr -> bool
+val is_sort : env -> evar_map -> types -> bool
 
-val contract_fix : ?env:Environ.env -> evar_map -> ?reference:Constant.t -> (EConstr.t, EConstr.t) pfixpoint -> EConstr.t
+val contract_fix : ?env:Environ.env -> evar_map -> ?reference:Constant.t -> fixpoint -> constr
 val fix_recarg : ('a, 'a) pfixpoint -> 'b Stack.t -> (int * 'b) option
 
 (** {6 Querying the kernel conversion oracle: opaque/transparent constants } *)
@@ -249,14 +248,14 @@ type conversion_test = constraints -> constraints
 val pb_is_equal : conv_pb -> bool
 val pb_equal : conv_pb -> conv_pb
 
-val is_conv : ?reds:transparent_state -> env -> evar_map -> EConstr.t -> EConstr.t -> bool
-val is_conv_leq : ?reds:transparent_state -> env ->  evar_map -> EConstr.t -> EConstr.t -> bool
-val is_fconv : ?reds:transparent_state -> conv_pb -> env ->  evar_map -> EConstr.t -> EConstr.t -> bool
+val is_conv : ?reds:transparent_state -> env -> evar_map -> constr -> constr -> bool
+val is_conv_leq : ?reds:transparent_state -> env ->  evar_map -> constr -> constr -> bool
+val is_fconv : ?reds:transparent_state -> conv_pb -> env ->  evar_map -> constr -> constr -> bool
 
 (** [check_conv] Checks universe constraints only.
     pb defaults to CUMUL and ts to a full transparent state.
  *)
-val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env ->  evar_map -> EConstr.t -> EConstr.t -> bool
+val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env ->  evar_map -> constr -> constr -> bool
 
 (** [infer_conv] Adds necessary universe constraints to the evar map.
     pb defaults to CUMUL and ts to a full transparent state.
@@ -264,29 +263,29 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env ->  evar_map -> ECo
     otherwise returns false in that case.
  *)
 val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> 
-  env -> evar_map -> EConstr.constr -> EConstr.constr -> evar_map * bool
+  env -> evar_map -> constr -> constr -> evar_map * bool
 
 (** Conversion with inference of universe constraints *)
-val set_vm_infer_conv : (?pb:conv_pb -> env -> evar_map -> EConstr.constr -> EConstr.constr ->
+val set_vm_infer_conv : (?pb:conv_pb -> env -> evar_map -> constr -> constr ->
   evar_map * bool) -> unit
-val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> EConstr.constr -> EConstr.constr ->
+val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
   evar_map * bool
 
 
 (** [infer_conv_gen] behaves like [infer_conv] but is parametrized by a
 conversion function. Used to pretype vm and native casts. *)
 val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state ->
-    (constr, evar_map) Reduction.generic_conversion_function) ->
+    (Constr.constr, evar_map) Reduction.generic_conversion_function) ->
   ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> env ->
-  evar_map -> EConstr.constr -> EConstr.constr -> evar_map * bool
+  evar_map -> constr -> constr -> evar_map * bool
 
 (** {6 Special-Purpose Reduction Functions } *)
 
 val whd_meta : local_reduction_function
-val plain_instance : evar_map -> EConstr.t Metamap.t -> EConstr.t -> EConstr.t
-val instance : evar_map -> EConstr.t Metamap.t -> EConstr.t -> constr
+val plain_instance : evar_map -> constr Metamap.t -> constr -> constr
+val instance : evar_map -> constr Metamap.t -> constr -> constr
 val head_unfold_under_prod : transparent_state -> reduction_function
-val betazetaevar_applist : evar_map -> int -> EConstr.t -> EConstr.t list -> constr
+val betazetaevar_applist : evar_map -> int -> constr -> constr list -> constr
 
 (** {6 Heuristic for Conversion with Evar } *)
 
@@ -295,6 +294,6 @@ val whd_betaiota_deltazeta_for_iota_state :
   state * Cst_stack.t
 
 (** {6 Meta-related reduction functions } *)
-val meta_instance : evar_map -> EConstr.constr freelisted -> EConstr.constr
-val nf_meta       : evar_map -> EConstr.constr -> EConstr.constr
-val meta_reducible_instance : evar_map -> EConstr.constr freelisted -> EConstr.constr
+val meta_instance : evar_map -> constr freelisted -> constr
+val nf_meta       : evar_map -> constr -> constr
+val meta_reducible_instance : evar_map -> constr freelisted -> constr
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 3142ea5cb..7db30bf23 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -74,7 +74,7 @@ let get_type_from_constraints env sigma t =
 let rec subst_type env sigma typ = function
   | [] -> typ
   | h::rest ->
-      match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma typ)) with
+      match EConstr.kind sigma (whd_all env sigma typ) with
         | Prod (na,c1,c2) -> subst_type env sigma (subst1 h c2) rest
         | _ -> retype_error NonFunctionalConstruction
 
@@ -83,7 +83,7 @@ let rec subst_type env sigma typ = function
 
 let sort_of_atomic_type env sigma ft args =
   let rec concl_of_arity env n ar args =
-    match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma ar)), args with
+    match EConstr.kind sigma (whd_all env sigma ar), args with
     | Prod (na, t, b), h::l -> concl_of_arity (push_rel (local_def (na, lift n h, t)) env) (n + 1) b l
     | Sort s, [] -> s
     | _ -> retype_error NotASort
@@ -94,7 +94,7 @@ let type_of_var env id =
   with Not_found -> retype_error (BadVariable id)
 
 let decomp_sort env sigma t =
-  match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with
+  match EConstr.kind sigma (whd_all env sigma t) with
   | Sort s -> s
   | _ -> retype_error NotASort
 
@@ -123,9 +123,9 @@ let retype ?(polyprop=true) sigma =
           with Not_found -> retype_error BadRecursiveType
         in
         let n = inductive_nrealdecls_env env (fst (fst (dest_ind_family indf))) in
-        let t = EConstr.of_constr (betazetaevar_applist sigma n p realargs) in
-        (match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma (type_of env t))) with
-          | Prod _ -> EConstr.of_constr (whd_beta sigma (applist (t, [c])))
+        let t = betazetaevar_applist sigma n p realargs in
+        (match EConstr.kind sigma (whd_all env sigma (type_of env t)) with
+          | Prod _ -> whd_beta sigma (applist (t, [c]))
           | _ -> t)
     | Lambda (name,c1,c2) ->
           mkProd (name, c1, type_of (push_rel (local_assum (name,c1)) env) c2)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 1d179c683..02524f896 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -425,7 +425,7 @@ 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 rec check strict c =
-    let c' = EConstr.of_constr (whd_betaiotazeta sigma c) in
+    let c' = whd_betaiotazeta sigma c in
     let (h,rcargs) = decompose_app_vect sigma c' in
     match EConstr.kind sigma h with
         Evar(i,_) when Evar.Map.mem i fxminargs && not (Evd.is_defined !evm i) ->
@@ -473,7 +473,7 @@ let reduce_fix whdfun sigma fix stack =
     | None -> NotReducible
     | Some (recargnum,recarg) ->
         let (recarg'hd,_ as recarg') = whdfun sigma recarg in
-        let stack' = List.assign stack recargnum (EConstr.applist recarg') in
+        let stack' = List.assign stack recargnum (applist recarg') in
 	(match EConstr.kind sigma recarg'hd with
            | Construct _ -> Reduced (contract_fix sigma fix, stack')
 	   | _ -> NotReducible)
@@ -483,7 +483,7 @@ let contract_fix_use_function env sigma f
   let nbodies = Array.length recindices in
   let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in
   let lbodies = List.init nbodies make_Fi in
-  substl_checking_arity env (List.rev lbodies) sigma (EConstr.of_constr (nf_beta sigma bodies.(bodynum)))
+  substl_checking_arity env (List.rev lbodies) sigma (nf_beta sigma bodies.(bodynum))
 
 let reduce_fix_use_function env sigma f whfun fix stack =
   match fix_recarg fix (Stack.append_app_list stack Stack.empty) with
@@ -495,7 +495,7 @@ let reduce_fix_use_function env sigma f whfun fix stack =
 	    (recarg, [])
 	  else
 	    whfun recarg in
-        let stack' = List.assign stack recargnum (EConstr.applist recarg') in
+        let stack' = List.assign stack recargnum (applist recarg') in
 	(match EConstr.kind sigma recarg'hd with
            | Construct _ ->
 	       Reduced (contract_fix_use_function env sigma f fix,stack')
@@ -507,7 +507,7 @@ let contract_cofix_use_function env sigma f
   let make_Fi j = (mkCoFix(j,typedbodies), f j) in
   let subbodies = List.init nbodies make_Fi in
   substl_checking_arity env (List.rev subbodies)
-    sigma (EConstr.of_constr (nf_beta sigma bodies.(bodynum)))
+    sigma (nf_beta sigma bodies.(bodynum))
 
 let reduce_mind_case_use_function func env sigma mia =
   match EConstr.kind sigma mia.mconstr with
@@ -689,7 +689,7 @@ let rec red_elim_const env sigma ref u largs =
 	let whfun = whd_construct_stack env sigma in
 	(match reduce_fix_use_function env sigma f whfun (destFix sigma d) lrest with
 	   | NotReducible -> raise Redelimination
-           | Reduced (c,rest) -> (EConstr.of_constr (nf_beta sigma c), rest), nocase)
+           | Reduced (c,rest) -> (nf_beta sigma c, rest), nocase)
     | EliminationMutualFix (min,refgoal,refinfos) when nargs >= min ->
 	let rec descend (ref,u) args =
 	  let c = reference_value env sigma ref u in
@@ -704,14 +704,14 @@ let rec red_elim_const env sigma ref u largs =
 	let whfun = whd_construct_stack env sigma in
 	(match reduce_fix_use_function env sigma f whfun (destFix sigma d) lrest with
 	   | NotReducible -> raise Redelimination
-	   | Reduced (c,rest) -> (EConstr.of_constr (nf_beta sigma c), rest), nocase)
+	   | Reduced (c,rest) -> (nf_beta sigma c, rest), nocase)
     | NotAnElimination when unfold_nonelim ->
          let c = reference_value env sigma ref u in
-           (EConstr.of_constr (whd_betaiotazeta sigma (applist (c, largs))), []), nocase
+           (whd_betaiotazeta sigma (applist (c, largs)), []), nocase
     | _ -> raise Redelimination
     with Redelimination when unfold_anyway ->
        let c = reference_value env sigma ref u in
-	 (EConstr.of_constr (whd_betaiotazeta sigma (applist (c, largs))), []), nocase
+	 (whd_betaiotazeta sigma (applist (c, largs)), []), nocase
 
 and reduce_params env sigma stack l =
   let len = List.length stack in
@@ -721,7 +721,7 @@ and reduce_params env sigma stack l =
 	let arg = List.nth stack i in
 	let rarg = whd_construct_stack env sigma arg in
 	  match EConstr.kind sigma (fst rarg) with
-	  | Construct _ -> List.assign stack i (EConstr.applist rarg)
+	  | Construct _ -> List.assign stack i (applist rarg)
 	  | _ -> raise Redelimination)
       stack l
     
@@ -817,9 +817,9 @@ and whd_construct_stack env sigma s =
 *)
 
 let try_red_product env sigma c =
-  let simpfun c = EConstr.of_constr (clos_norm_flags betaiotazeta env sigma c) in
+  let simpfun c = clos_norm_flags betaiotazeta env sigma c in
   let rec redrec env x =
-    let x = EConstr.of_constr (whd_betaiota sigma x) in
+    let x = whd_betaiota sigma x in
     match EConstr.kind sigma x with
       | App (f,l) ->
           (match EConstr.kind sigma f with
@@ -856,7 +856,7 @@ let try_red_product env sigma c =
 	     | None -> raise Redelimination
 	     | Some c -> c)
 	| _ -> raise Redelimination)
-  in EConstr.Unsafe.to_constr (redrec env c)
+  in redrec env c
 
 let red_product env sigma c =
   try try_red_product env sigma c
@@ -953,7 +953,7 @@ let hnf_constr = whd_simpl_orelse_delta_but_fix
 (* The "simpl" reduction tactic *)
 
 let whd_simpl env sigma c =
-  EConstr.Unsafe.to_constr (EConstr.applist (whd_simpl_stack env sigma c))
+  applist (whd_simpl_stack env sigma c)
 
 let simpl env sigma c = strong whd_simpl env sigma c
 
@@ -1010,7 +1010,7 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t ->
         if locs != [] then
           ignore (traverse_below (Some (!pos-1)) envc t);
 	let Sigma (t, evm, _) = (f subst).e_redfun env (Sigma.Unsafe.of_evar_map !evd) t in
-	(evd := Sigma.to_evar_map evm; EConstr.of_constr t)
+	(evd := Sigma.to_evar_map evm; t)
       end
       else
 	traverse_below nested envc t
@@ -1029,7 +1029,7 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t ->
   in
   let t' = traverse None (env,c) t in
   if List.exists (fun o -> o >= !pos) locs then error_invalid_occurrence locs;
-  Sigma.Unsafe.of_pair (EConstr.Unsafe.to_constr t', !evd)
+  Sigma.Unsafe.of_pair (t', !evd)
   end }
 
 let contextually byhead occs f env sigma t =
@@ -1080,7 +1080,7 @@ let string_of_evaluable_ref env = function
 
 let unfold env sigma name c =
   if is_evaluable env name then
-    EConstr.of_constr (clos_norm_flags (unfold_red name) env sigma c)
+    clos_norm_flags (unfold_red name) env sigma c
   else
     error (string_of_evaluable_ref env name^" is opaque.")
 
@@ -1098,7 +1098,7 @@ let unfoldoccs env sigma (occs,name) c =
     | [] -> ()
     | _ -> error_invalid_occurrence rest
     in
-    EConstr.of_constr (nf_betaiotazeta sigma uc)
+    nf_betaiotazeta sigma uc
   in
   match occs with
     | NoOccurrences -> c
@@ -1108,17 +1108,17 @@ let unfoldoccs env sigma (occs,name) c =
 
 (* Unfold reduction tactic: *)
 let unfoldn loccname env sigma c =
-  EConstr.Unsafe.to_constr (List.fold_left (fun c occname -> unfoldoccs env sigma occname c) c loccname)
+  List.fold_left (fun c occname -> unfoldoccs env sigma occname c) c loccname
 
 (* Re-folding constants tactics: refold com in term c *)
 let fold_one_com com env sigma c =
   let rcom =
-    try EConstr.of_constr (red_product env sigma com)
+    try red_product env sigma com
     with Redelimination -> error "Not reducible." in
   (* Reason first on the beta-iota-zeta normal form of the constant as
      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 = subst_term sigma (clos_norm_flags unfold_side_red env sigma rcom) c in
   if not (EConstr.eq_constr sigma a c) then
     Vars.subst1 com a
   else
@@ -1128,12 +1128,12 @@ let fold_one_com com env sigma c =
     Vars.subst1 com a
 
 let fold_commands cl env sigma c =
-  EConstr.Unsafe.to_constr (List.fold_right (fun com c -> fold_one_com com env sigma c) (List.rev cl) c)
+  List.fold_right (fun com c -> fold_one_com com env sigma c) (List.rev cl) c
 
 
 (* call by value reduction functions *)
 let cbv_norm_flags flags env sigma t =
-  cbv_norm (create_cbv_infos flags env sigma) t
+  EConstr.of_constr (cbv_norm (create_cbv_infos flags env sigma) t)
 
 let cbv_beta = cbv_norm_flags beta empty_env
 let cbv_betaiota = cbv_norm_flags betaiota empty_env
@@ -1163,7 +1163,7 @@ let pattern_occs loccs_trm = { e_redfun = begin fun env sigma c ->
   let abstr_trm, sigma = List.fold_right (abstract_scheme env sigma) loccs_trm (c,sigma) in
   try
     let _ = Typing.unsafe_type_of env sigma abstr_trm in
-    Sigma.Unsafe.of_pair (EConstr.Unsafe.to_constr (applist(abstr_trm, List.map snd loccs_trm)), sigma)
+    Sigma.Unsafe.of_pair (applist(abstr_trm, List.map snd loccs_trm), sigma)
   with Type_errors.TypeError (env',t) ->
     raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t))))
   end }
@@ -1189,7 +1189,6 @@ let check_not_primitive_record env ind =
 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 (fst (decompose_app_vect sigma t)) with
       | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t l)
       | Prod (n,ty,t') ->
@@ -1202,7 +1201,6 @@ let reduce_to_ind_gen allow_product env sigma t =
 	  (* Last chance: we allow to bypass the Opaque flag (as it
 	     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 (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.")
@@ -1285,7 +1283,6 @@ let reduce_to_ref_gen allow_product env sigma ref t =
 	  with Not_found ->
           try
 	    let t' = nf_betaiota sigma (one_step_reduce env sigma t) in
-	    let t' = EConstr.of_constr t' in
             elimrec env t' l
           with NotStepReducible -> error_cannot_recognize ref
   in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index f59a6dcd9..9ee34341b 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -291,6 +291,7 @@ let build_subclasses ~check env sigma glob pri =
 	let instapp = 
 	  Reductionops.whd_beta sigma (EConstr.of_constr (appvectc c (Context.Rel.to_extended_vect 0 rels)))
 	in
+	let instapp = EConstr.Unsafe.to_constr instapp in
 	let projargs = Array.of_list (args @ [instapp]) in
 	let projs = List.map_filter 
 	  (fun (n, b, proj) ->
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 40ef2450a..f67e0bddc 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -53,7 +53,7 @@ let inductive_type_knowing_parameters env sigma (ind,u) jl =
   EConstr.of_constr (Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp)
 
 let e_type_judgment env evdref j =
-  match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref j.uj_type)) with
+  match EConstr.kind !evdref (whd_all env !evdref j.uj_type) with
     | Sort s -> {utj_val = j.uj_val; utj_type = s }
     | Evar ev ->
         let (evd,s) = Evardefine.define_evar_as_sort env !evdref ev in
@@ -71,7 +71,7 @@ let e_judge_of_apply env evdref funj argjv =
       { uj_val  = mkApp (j_val funj, Array.map j_val argjv);
         uj_type = typ }
   | hj::restjl ->
-      match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref typ)) with
+      match EConstr.kind !evdref (whd_all env !evdref typ) with
       | Prod (_,c1,c2) ->
 	 if Evarconv.e_cumul env evdref hj.uj_type c1 then
 	   apply_rec (n+1) (subst1 hj.uj_val c2) restjl
@@ -104,7 +104,7 @@ let e_is_correct_arity env evdref c pj ind specif params =
   let allowed_sorts = elim_sorts specif in
   let error () = Pretype_errors.error_elim_arity env !evdref ind allowed_sorts c pj None in
   let rec srec env pt ar =
-    let pt' = EConstr.of_constr (whd_all env !evdref pt) in
+    let pt' = whd_all env !evdref pt in
     match EConstr.kind !evdref pt', ar with
     | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
         if not (Evarconv.e_cumul env evdref a1 (EConstr.of_constr a1')) then error ();
@@ -144,7 +144,6 @@ let e_type_case_branches env evdref (ind,largs) pj c =
   let lc = Array.map EConstr.of_constr lc in
   let n = (snd specif).Declarations.mind_nrealdecls in
   let ty = whd_betaiota !evdref (lambda_applist_assum !evdref (n+1) p (realargs@[c])) in
-  let ty = EConstr.of_constr ty in
   (lc, ty)
 
 let e_judge_of_case env evdref ci pj cj lfj =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 169dd45bc..8a8649f11 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -75,7 +75,6 @@ let occur_meta_evd sigma mv c =
   let rec occrec c =
     (* Note: evars are not instantiated by terms with metas *)
     let c = whd_meta sigma c in
-    let c = EConstr.of_constr c in
     match EConstr.kind sigma c with
     | Meta mv' when Int.equal mv mv' -> raise Occur
     | _ -> EConstr.iter sigma occrec c
@@ -1003,24 +1002,24 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
 	    (match expand_key flags.modulo_delta curenv sigma cf1 with
 	    | Some c ->
 		unirec_rec curenvnb pb opt substn
-                  (EConstr.of_constr (whd_betaiotazeta sigma (mkApp(c,l1)))) cN
+                  (whd_betaiotazeta sigma (mkApp(c,l1))) cN
 	    | None ->
 		(match expand_key flags.modulo_delta curenv sigma cf2 with
 		| Some c ->
 		    unirec_rec curenvnb pb opt substn cM
-                      (EConstr.of_constr (whd_betaiotazeta sigma (mkApp(c,l2))))
+                      (whd_betaiotazeta sigma (mkApp(c,l2)))
 		| None ->
 		    error_cannot_unify curenv sigma (cM,cN)))
 	| Some false ->
 	    (match expand_key flags.modulo_delta curenv sigma cf2 with
 	    | Some c ->
 		unirec_rec curenvnb pb opt substn cM
-                  (EConstr.of_constr (whd_betaiotazeta sigma (mkApp(c,l2))))
+                  (whd_betaiotazeta sigma (mkApp(c,l2)))
 	    | None ->
 		(match expand_key flags.modulo_delta curenv sigma cf1 with
 		| Some c ->
 		    unirec_rec curenvnb pb opt substn
-                      (EConstr.of_constr (whd_betaiotazeta sigma (mkApp(c,l1)))) cN
+                      (whd_betaiotazeta sigma (mkApp(c,l1))) cN
 		| None ->
 		    error_cannot_unify curenv sigma (cM,cN)))
 
@@ -1233,7 +1232,7 @@ let applyHead env (type r) (evd : r Sigma.t) n c =
       Sigma (c, evd, p)
     else
       let sigma = Sigma.to_evar_map evd in
-      match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma cty)) with
+      match EConstr.kind sigma (whd_all env sigma cty) with
       | Prod (_,c1,c2) ->
         let Sigma (evar, evd', q) = Evarutil.new_evar env evd ~src:(Loc.ghost,Evar_kinds.GoalEvar) c1 in
 	  apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd'
@@ -1263,7 +1262,7 @@ let w_coerce_to_type env evd c cty mvty =
        but there are cases where it though it was not rigid (like in
        fst (nat,nat)) and stops while it could have seen that it is rigid *)
     let cty = Tacred.hnf_constr env evd cty in
-      try_to_coerce env evd c (EConstr.of_constr cty) tycon
+      try_to_coerce env evd c cty tycon
 	  
 let w_coerce env evd mv c =
   let cty = get_type_of env evd c in
@@ -1276,7 +1275,6 @@ let unify_to_type env sigma flags c status u =
   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
-  let t = EConstr.of_constr t in
     unify_0 env sigma CUMUL flags t u
 
 let unify_type env sigma flags mv status c =
@@ -1379,7 +1377,7 @@ let w_merge env with_types flags (evd,metas,evars : subst0) =
     	  else
             let evd' =
               if occur_meta_evd evd mv c then
-                if isMetaOf mv (whd_all env evd c) then evd
+                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
@@ -1618,7 +1616,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
   (fun test -> match test.testing_state with
   | None -> None
   | Some (sigma,_,l) ->
-     let c = applist (EConstr.of_constr (nf_evar sigma (local_strong whd_meta sigma c)), l) in
+     let c = applist (EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr (local_strong whd_meta sigma c))), l) in
      let univs, subst = nf_univ_variables sigma in
      Some (sigma,EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr c))))
 
@@ -1877,7 +1875,6 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t =
   List.fold_right
     (fun op (evd,l) ->
       let op = whd_meta evd op in
-      let op = EConstr.of_constr op in
       if isMeta evd op then
 	if flags.allow_K_in_toplevel_higher_order_unification then (evd,op::l)
 	else error_abstraction_over_meta env evd hdmeta (destMeta evd op)
@@ -1983,8 +1980,8 @@ let w_unify2 env evd flags dep cv_pb ty1 ty2 =
    convertible and first-order otherwise. But if failed if e.g. the type of
    Meta(1) had meta-variables in it. *)
 let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 =
-  let hd1,l1 = decompose_app_vect evd (EConstr.of_constr (whd_nored evd ty1)) in
-  let hd2,l2 = decompose_app_vect evd (EConstr.of_constr (whd_nored evd ty2)) in
+  let hd1,l1 = decompose_app_vect evd (whd_nored evd ty1) in
+  let hd2,l2 = decompose_app_vect evd (whd_nored evd ty2) in
   let is_empty1 = Array.is_empty l1 in
   let is_empty2 = Array.is_empty l2 in
     match EConstr.kind evd hd1, not is_empty1, EConstr.kind evd hd2, not is_empty2 with
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 31693d82f..74998349b 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -360,7 +360,7 @@ let cbv_vm env sigma c t  =
   let c = EConstr.to_constr sigma c in
   let t = EConstr.to_constr sigma t in
   let v = Vconv.val_of_constr env c in
-  nf_val env sigma v t
+  EConstr.of_constr (nf_val env sigma v t)
 
 let vm_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 =
   Reductionops.infer_conv_gen (fun pb ~l2r sigma ts -> Vconv.vm_conv_gen pb)
diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli
index 650f3f291..8a4202c88 100644
--- a/pretyping/vnorm.mli
+++ b/pretyping/vnorm.mli
@@ -10,4 +10,4 @@ open EConstr
 open Environ
 
 (** {6 Reduction functions } *)
-val cbv_vm : env -> Evd.evar_map -> constr -> types -> Constr.t
+val cbv_vm : env -> Evd.evar_map -> constr -> types -> constr