Tacred API using EConstr.

14 files changed, 212 insertions, 160 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index 26b22be4e..f191e2dc1 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -320,8 +320,19 @@ let map_constr_with_named_binders g f l c = match kind_of_term c with
    time being almost those of the ML representation (except for
    (co-)fixpoint) *)
 
+let local_assum (na, t) =
+  let open RelDecl in
+  let inj = EConstr.Unsafe.to_constr in
+  LocalAssum (na, inj t)
+
+let local_def (na, b, t) =
+  let open RelDecl in
+  let inj = EConstr.Unsafe.to_constr in
+  LocalDef (na, inj b, inj t)
+
 let fold_rec_types g (lna,typarray,_) e =
-  let ctxt = Array.map2_i (fun i na t -> RelDecl.LocalAssum (na, lift i t)) lna typarray in
+  let open EConstr in
+  let ctxt = Array.map2_i (fun i na t -> local_assum (na, Vars.lift i t)) lna typarray in
   Array.fold_left (fun e assum -> g assum e) e ctxt
 
 let map_left2 f a g b =
@@ -336,9 +347,9 @@ let map_left2 f a g b =
     r, s
   end
 
-let map_constr_with_binders_left_to_right g f l c =
-  let open RelDecl in
-  match kind_of_term c with
+let map_constr_with_binders_left_to_right sigma g f l c =
+  let open EConstr in
+  match EConstr.kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> c
   | Cast (b,k,t) -> 
@@ -348,18 +359,18 @@ let map_constr_with_binders_left_to_right g f l c =
       else mkCast (b',k,t')
   | Prod (na,t,b) ->
       let t' = f l t in
-      let b' = f (g (LocalAssum (na,t)) l) b in
+      let b' = f (g (local_assum (na,t)) l) b in
 	if t' == t && b' == b then c
 	else mkProd (na, t', b')
   | Lambda (na,t,b) ->
       let t' = f l t in
-      let b' = f (g (LocalAssum (na,t)) l) b in
+      let b' = f (g (local_assum (na,t)) l) b in
 	if t' == t && b' == b then c
 	else mkLambda (na, t', b')
   | LetIn (na,bo,t,b) ->
       let bo' = f l bo in
       let t' = f l t in
-      let b' = f (g (LocalDef (na,bo,t)) l) b in
+      let b' = f (g (local_def (na,bo,t)) l) b in
 	if bo' == bo && t' == t && b' == b then c
 	else mkLetIn (na, bo', t', b')	    
   | App (c,[||]) -> assert false
diff --git a/engine/termops.mli b/engine/termops.mli
index 24c2c82f2..4becca907 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -65,9 +65,10 @@ val map_constr_with_named_binders :
   (Name.t -> 'a -> 'a) ->
   ('a -> constr -> constr) -> 'a -> constr -> constr
 val map_constr_with_binders_left_to_right :
+  Evd.evar_map ->
   (Context.Rel.Declaration.t -> 'a -> 'a) ->
-  ('a -> constr -> constr) ->
-    'a -> constr -> constr
+  ('a -> EConstr.constr -> EConstr.constr) ->
+    'a -> EConstr.constr -> EConstr.constr
 val map_constr_with_full_binders :
   Evd.evar_map ->
   (Context.Rel.Declaration.t -> 'a -> 'a) ->
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index ca1f6e638..e1b468197 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -300,7 +300,7 @@ let project_hint pri l2r r =
   let sigma, c = Evd.fresh_global env sigma gr in
   let t = Retyping.get_type_of env sigma (EConstr.of_constr c) in
   let t =
-    Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) t in
+    Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) (EConstr.of_constr t) in
   let sign,ccl = decompose_prod_assum t in
   let (a,b) = match snd (decompose_app ccl) with
     | [a;b] -> (a,b)
@@ -738,7 +738,7 @@ let  mkCaseEq a  : unit Proofview.tactic =
             let concl = Proofview.Goal.concl gl in
             let env = Proofview.Goal.env gl in
             (** FIXME: this looks really wrong. Does anybody really use this tactic? *)
-            let Sigma (c, _, _) = (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a]).Reductionops.e_redfun env (Sigma.Unsafe.of_evar_map Evd.empty) (EConstr.of_constr concl) in
+            let Sigma (c, _, _) = (Tacred.pattern_occs [Locus.OnlyOccurrences [1], EConstr.of_constr a]).Reductionops.e_redfun env (Sigma.Unsafe.of_evar_map Evd.empty) (EConstr.of_constr concl) in
 	    change_concl c
           end };
 	  simplest_case a]
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 12ed758ba..bdbf0242d 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -692,7 +692,7 @@ let mkDestructEq :
      [Proofview.V82.of_tactic (generalize new_hyps);
       (fun g2 ->
         let changefun patvars = { run = fun sigma ->
-          let redfun = pattern_occs [Locus.AllOccurrencesBut [1], expr] in
+          let redfun = pattern_occs [Locus.AllOccurrencesBut [1], EConstr.of_constr expr] in
           redfun.Reductionops.e_redfun (pf_env g2) sigma (EConstr.of_constr (pf_concl g2))
         } in
 	Proofview.V82.of_tactic (change_in_concl None changefun) g2);
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index e0d99d453..18aeca6fa 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -836,7 +836,10 @@ let rec uniquize = function
           | Context.Rel.Declaration.LocalDef (x,_,y) ->
               Context.Rel.Declaration.LocalAssum(x,y) in
         Environ.push_rel ctx_item env, h' + 1 in
-      let f' = map_constr_with_binders_left_to_right inc_h subst_loop acc f in
+      let self acc c = EConstr.of_constr (subst_loop acc (EConstr.Unsafe.to_constr c)) in
+      let f = EConstr.of_constr f in
+      let f' = map_constr_with_binders_left_to_right sigma inc_h self acc f in
+      let f' = EConstr.Unsafe.to_constr f' in
       mkApp (f', Array.map_left (subst_loop acc) a) in
   subst_loop (env,h) c) : find_P),
 ((fun () ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index c8dcb19b4..cdcb993b5 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -986,10 +986,9 @@ let apply_on_subterm env evdref f c t =
           let g decl a = if is_local_assum decl then applyrec acc a else a in
           mkEvar (evk, Array.of_list (List.map2 g ctx (Array.to_list args)))
       | _ ->
-        let self acc c = EConstr.Unsafe.to_constr (applyrec acc (EConstr.of_constr c)) in
-        EConstr.of_constr (map_constr_with_binders_left_to_right
+        map_constr_with_binders_left_to_right !evdref
 	  (fun d (env,(k,c)) -> (push_rel d env, (k+1,Vars.lift 1 c)))
-	  self acc (EConstr.Unsafe.to_constr t))
+	  applyrec acc t
   in
   applyrec (env,(0,c)) t
 
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index d7f2d54aa..2b243d5b9 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -99,7 +99,7 @@ type 'a testing_function = {
    (b,l), b=true means no occurrence except the ones in l and b=false,
    means all occurrences except the ones in l *)
 
-let replace_term_occ_gen_modulo occs like_first test bywhat cl occ t =
+let replace_term_occ_gen_modulo sigma occs like_first test bywhat cl occ t =
   let (nowhere_except_in,locs) = Locusops.convert_occs occs in
   let maxocc = List.fold_right max locs 0 in
   let pos = ref occ in
@@ -133,24 +133,23 @@ let replace_term_occ_gen_modulo occs like_first test bywhat cl occ t =
     with NotUnifiable _ ->
       subst_below k t
   and subst_below k t =
-    let substrec i c = EConstr.Unsafe.to_constr (substrec i (EConstr.of_constr c)) in
-    EConstr.of_constr (map_constr_with_binders_left_to_right (fun d k -> k+1) substrec k (EConstr.Unsafe.to_constr t))
+    map_constr_with_binders_left_to_right sigma (fun d k -> k+1) substrec k t
   in
   let t' = substrec 0 t in
   (!pos, t')
 
-let replace_term_occ_modulo occs test bywhat t =
+let replace_term_occ_modulo evd occs test bywhat t =
   let occs',like_first =
     match occs with AtOccs occs -> occs,false | LikeFirst -> AllOccurrences,true in
   EConstr.Unsafe.to_constr (proceed_with_occurrences
-    (replace_term_occ_gen_modulo occs' like_first test bywhat None) occs' t)
+    (replace_term_occ_gen_modulo evd occs' like_first test bywhat None) occs' t)
 
-let replace_term_occ_decl_modulo occs test bywhat d =
+let replace_term_occ_decl_modulo evd occs test bywhat d =
   let (plocs,hyploc),like_first =
     match occs with AtOccs occs -> occs,false | LikeFirst -> (AllOccurrences,InHyp),true in
   proceed_with_occurrences
     (map_named_declaration_with_hyploc
-       (replace_term_occ_gen_modulo plocs like_first test bywhat)
+       (replace_term_occ_gen_modulo evd plocs like_first test bywhat)
        hyploc)
     plocs d
 
@@ -172,7 +171,7 @@ let make_eq_univs_test env evd c =
 let subst_closed_term_occ env evd occs c t =
   let test = make_eq_univs_test env evd c in
   let bywhat () = mkRel 1 in
-  let t' = replace_term_occ_modulo occs test bywhat t in
+  let t' = replace_term_occ_modulo evd occs test bywhat t in
     t', test.testing_state
 
 let subst_closed_term_occ_decl env evd occs c d =
@@ -182,6 +181,6 @@ let subst_closed_term_occ_decl env evd occs c d =
   let bywhat () = mkRel 1 in
   proceed_with_occurrences
     (map_named_declaration_with_hyploc
-       (fun _ -> replace_term_occ_gen_modulo plocs like_first test bywhat None)
+       (fun _ -> replace_term_occ_gen_modulo evd plocs like_first test bywhat None)
        hyploc) plocs d,
   test.testing_state
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli
index 49a5dd7f2..e7f0da93f 100644
--- a/pretyping/find_subterm.mli
+++ b/pretyping/find_subterm.mli
@@ -41,12 +41,13 @@ val make_eq_univs_test : env -> evar_map -> EConstr.constr -> evar_map testing_f
     matching subterms at the indicated occurrences [occl] with [mk
     ()]; it turns a NotUnifiable exception raised by the testing
     function into a SubtermUnificationError. *)
-val replace_term_occ_modulo : occurrences or_like_first ->
+val replace_term_occ_modulo : evar_map -> occurrences or_like_first ->
   'a testing_function -> (unit -> EConstr.constr) -> EConstr.constr -> constr
 
 (** [replace_term_occ_decl_modulo] is similar to
     [replace_term_occ_modulo] but for a named_declaration. *)
 val replace_term_occ_decl_modulo :
+  evar_map ->
   (occurrences * hyp_location_flag) or_like_first ->
   'a testing_function -> (unit -> EConstr.constr) ->
   Context.Named.Declaration.t -> Context.Named.Declaration.t
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 9581db23d..9997976c4 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -31,7 +31,7 @@ module NamedDecl = Context.Named.Declaration
 (* Errors *)
 
 type reduction_tactic_error =
-    InvalidAbstraction of env * Evd.evar_map * constr * (env * Type_errors.type_error)
+    InvalidAbstraction of env * Evd.evar_map * EConstr.constr * (env * Type_errors.type_error)
 
 exception ReductionTacticError of reduction_tactic_error
 
@@ -77,14 +77,14 @@ type evaluable_reference =
   | EvalConst of constant
   | EvalVar of Id.t
   | EvalRel of int
-  | EvalEvar of existential
+  | EvalEvar of EConstr.existential
 
-let evaluable_reference_eq r1 r2 = match r1, r2 with
+let evaluable_reference_eq sigma r1 r2 = match r1, r2 with
 | EvalConst c1, EvalConst c2 -> eq_constant c1 c2
 | EvalVar id1, EvalVar id2 -> Id.equal id1 id2
 | EvalRel i1, EvalRel i2 -> Int.equal i1 i2
 | EvalEvar (e1, ctx1), EvalEvar (e2, ctx2) ->
-  Evar.equal e1 e2 && Array.equal eq_constr ctx1 ctx2
+  Evar.equal e1 e2 && Array.equal (EConstr.eq_constr sigma) ctx1 ctx2
 | _ -> false
 
 let mkEvalRef ref u =
@@ -93,15 +93,15 @@ let mkEvalRef ref u =
   | EvalConst cst -> mkConstU (cst,u)
   | EvalVar id -> mkVar id
   | EvalRel n -> mkRel n
-  | EvalEvar ev -> EConstr.of_constr (Constr.mkEvar ev)
+  | EvalEvar ev -> EConstr.mkEvar ev
 
-let isEvalRef env c = match kind_of_term c with
+let isEvalRef env sigma c = match EConstr.kind sigma c with
   | Const (sp,_) -> is_evaluable env (EvalConstRef sp)
   | Var id -> is_evaluable env (EvalVarRef id)
   | Rel _ | Evar _ -> true
   | _ -> false
 
-let destEvalRefU c = match kind_of_term c with
+let destEvalRefU sigma c = match EConstr.kind sigma c with
   | Const (cst,u) ->  EvalConst cst, u
   | Var id  -> (EvalVar id, Univ.Instance.empty)
   | Rel n -> (EvalRel n, Univ.Instance.empty)
@@ -109,31 +109,39 @@ let destEvalRefU c = match kind_of_term c with
   | _ -> anomaly (Pp.str "Not an unfoldable reference")
 
 let unsafe_reference_opt_value env sigma eval =
+  let open EConstr in
   match eval with
   | EvalConst cst ->
     (match (lookup_constant cst env).Declarations.const_body with 
-    | Declarations.Def c -> Some (Mod_subst.force_constr c)
+    | Declarations.Def c -> Some (EConstr.of_constr (Mod_subst.force_constr c))
     | _ -> None)
   | EvalVar id ->
-      env |> lookup_named id |> NamedDecl.get_value
+      env |> lookup_named id |> NamedDecl.get_value |> Option.map EConstr.of_constr
   | EvalRel n ->
-      env |> lookup_rel n |> RelDecl.map_value (lift n) |> RelDecl.get_value
-  | EvalEvar ev -> Evd.existential_opt_value sigma ev
+      env |> lookup_rel n |> RelDecl.map_value (lift n) |> RelDecl.get_value |> Option.map EConstr.of_constr
+  | EvalEvar ev ->
+    match EConstr.kind sigma (mkEvar ev) with
+    | Evar _ -> None
+    | c -> Some (EConstr.of_kind c)
 
 let reference_opt_value env sigma eval u = 
+  let open EConstr in
   match eval with
-  | EvalConst cst -> constant_opt_value_in env (cst,u)
+  | EvalConst cst -> Option.map EConstr.of_constr (constant_opt_value_in env (cst,u))
   | EvalVar id ->
-      env |> lookup_named id |> NamedDecl.get_value
+      env |> lookup_named id |> NamedDecl.get_value |> Option.map EConstr.of_constr
   | EvalRel n ->
-      env |> lookup_rel n |> RelDecl.map_value (lift n) |> RelDecl.get_value
-  | EvalEvar ev -> Evd.existential_opt_value sigma ev
+      env |> lookup_rel n |> RelDecl.map_value (lift n) |> RelDecl.get_value |> Option.map EConstr.of_constr
+  | EvalEvar ev ->
+    match EConstr.kind sigma (mkEvar ev) with
+    | Evar _ -> None
+    | c -> Some (EConstr.of_kind c)
 
 exception NotEvaluable
 let reference_value env sigma c u =
   match reference_opt_value env sigma c u with
     | None -> raise NotEvaluable
-    | Some d -> EConstr.of_constr d
+    | Some d -> d
 
 (************************************************************************)
 (* Reduction of constants hiding a fixpoint (e.g. for "simpl" tactic).  *)
@@ -179,6 +187,7 @@ let eval_table = Summary.ref (Cmap.empty : frozen) ~name:"evaluation"
 *)
 
 let check_fix_reversibility sigma labs args ((lv,i),(_,tys,bds)) =
+  let open EConstr in
   let n = List.length labs in
   let nargs = List.length args in
   if nargs > n then raise Elimconst;
@@ -188,8 +197,8 @@ let check_fix_reversibility sigma labs args ((lv,i),(_,tys,bds)) =
       (function d -> match EConstr.kind sigma d with
          | Rel k ->
              if
-	       Array.for_all (noccurn k) tys
-	       && Array.for_all (noccurn (k+nbfix)) bds
+	       Array.for_all (Vars.noccurn sigma k) tys
+	       && Array.for_all (Vars.noccurn sigma (k+nbfix)) bds
 	       && k <= n
 	     then
 	       (k, List.nth labs (k-1))
@@ -223,6 +232,7 @@ let check_fix_reversibility sigma labs args ((lv,i),(_,tys,bds)) =
 
 let invert_name labs l na0 env sigma ref = function
   | Name id ->
+      let open EConstr in
       let minfxargs = List.length l in
       begin match na0 with
       | Name id' when Id.equal id' id ->
@@ -239,12 +249,13 @@ let invert_name labs l na0 env sigma ref = function
 	      try match unsafe_reference_opt_value env sigma ref with
 		| None -> None
 		| Some c ->
-		    let labs',ccl = decompose_lam c in
-		    let _, l' = whd_betalet_stack sigma (EConstr.of_constr ccl) in
+		    let labs',ccl = decompose_lam sigma c in
+		    let _, l' = whd_betalet_stack sigma ccl in
 		    let labs' = List.map snd labs' in
 		    (** ppedrot: there used to be generic equality on terms here *)
+                    let eq_constr c1 c2 = EConstr.eq_constr sigma c1 c2 in
 		    if List.equal eq_constr labs' labs &&
-                       List.equal (fun c1 c2 -> EConstr.eq_constr sigma c1 c2) l l' then Some (minfxargs,ref)
+                       List.equal eq_constr l l' then Some (minfxargs,ref)
                     else None
 	      with Not_found (* Undefined ref *) -> None
       end
@@ -254,20 +265,29 @@ let invert_name labs l na0 env sigma ref = function
    [compute_consteval_mutual_fix] only one by one, until finding the
    last one before the Fix if the latter is mutually defined *)
 
+let local_assum (na, t) =
+  let open Context.Rel.Declaration in
+  let inj = EConstr.Unsafe.to_constr in
+  LocalAssum (na, inj t)
+
+let local_def (na, b, t) =
+  let open Context.Rel.Declaration in
+  let inj = EConstr.Unsafe.to_constr in
+  LocalDef (na, inj b, inj t)
+
 let compute_consteval_direct env sigma ref =
+  let open EConstr in
   let rec srec env n labs onlyproj c =
-    let c',l = whd_betadeltazeta_stack env sigma (EConstr.of_constr c) in
-    let c' = EConstr.Unsafe.to_constr c' in
-    match kind_of_term c' with
+    let c',l = whd_betadeltazeta_stack env sigma c in
+    match EConstr.kind sigma c' with
       | Lambda (id,t,g) when List.is_empty l && not onlyproj ->
-          let open Context.Rel.Declaration in
-	  srec (push_rel (LocalAssum (id,t)) env) (n+1) (EConstr.of_constr t::labs) onlyproj g
+	  srec (push_rel (local_assum (id,t)) env) (n+1) (t::labs) onlyproj g
       | Fix fix when not onlyproj ->
 	  (try check_fix_reversibility sigma labs l fix
 	  with Elimconst -> NotAnElimination)
-      | Case (_,_,d,_) when isRel d && not onlyproj -> EliminationCases n
+      | Case (_,_,d,_) when isRel sigma d && not onlyproj -> EliminationCases n
       | Case (_,_,d,_) -> srec env n labs true d
-      | Proj (p, d) when isRel d -> EliminationProj n
+      | Proj (p, d) when isRel sigma d -> EliminationProj n
       | _ -> NotAnElimination
   in
   match unsafe_reference_opt_value env sigma ref with
@@ -275,14 +295,13 @@ let compute_consteval_direct env sigma ref =
     | Some c -> srec env 0 [] false c
 
 let compute_consteval_mutual_fix env sigma ref =
+  let open EConstr in
   let rec srec env minarg labs ref c =
-    let c',l = whd_betalet_stack sigma (EConstr.of_constr c) in
+    let c',l = whd_betalet_stack sigma c in
     let nargs = List.length l in
-    let c' = EConstr.Unsafe.to_constr c' in
-    match kind_of_term c' with
+    match EConstr.kind sigma c' with
       | Lambda (na,t,g) when List.is_empty l ->
-          let open Context.Rel.Declaration in
-	  srec (push_rel (LocalAssum (na,t)) env) (minarg+1) (t::labs) ref g
+	  srec (push_rel (local_assum (na,t)) env) (minarg+1) (t::labs) ref g
       | Fix ((lv,i),(names,_,_)) ->
 	  (* Last known constant wrapping Fix is ref = [labs](Fix l) *)
 	  (match compute_consteval_direct env sigma ref with
@@ -295,9 +314,9 @@ let compute_consteval_mutual_fix env sigma ref =
 		 let new_minarg = max (minarg'+minarg-nargs) minarg' in
 		 EliminationMutualFix (new_minarg,ref,(refs,infos))
 	     | _ -> assert false)
-      | _ when isEvalRef env c' ->
+      | _ when isEvalRef env sigma c' ->
 	  (* Forget all \'s and args and do as if we had started with c' *)
-	  let ref,_ = destEvalRefU c' in
+	  let ref,_ = destEvalRefU sigma c' in
 	  (match unsafe_reference_opt_value env sigma ref with
 	    | None -> anomaly (Pp.str "Should have been trapped by compute_direct")
 	    | Some c -> srec env (minarg-nargs) [] ref c)
@@ -417,23 +436,25 @@ 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
-    match kind_of_term h with
+    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
           if Array.length rcargs < minargs then
             if strict then set_fix i
             else raise Partial;
-          Array.iter (EConstr.of_constr %> check strict) rcargs
-      | (Var _|Const _) when isEvalRef env h ->
-          (let ev, u = destEvalRefU h in
+          Array.iter (check strict) rcargs
+      | (Var _|Const _) when isEvalRef env sigma h ->
+          (let ev, u = destEvalRefU sigma h in
 	     match reference_opt_value env sigma ev u with
              | Some h' ->
                 let bak = !evm in
-                (try Array.iter (EConstr.of_constr %> check false) rcargs
+                (try Array.iter (check false) rcargs
                 with Partial ->
                   evm := bak;
-                  check strict (EConstr.of_constr (Constr.mkApp(h',rcargs))))
-            | None -> Array.iter (EConstr.of_constr %> check strict) rcargs)
+                  check strict (mkApp(h',rcargs)))
+            | None -> Array.iter (check strict) rcargs)
       | _ -> EConstr.iter sigma (check strict) c' in
   check true c;
   !evm
@@ -445,14 +466,16 @@ let substl_checking_arity env subst sigma c =
   let sigma' = solve_arity_problem env sigma minargs body in
   (* we propagate the constraints: solved problems are substituted;
      the other ones are replaced by the function symbol *)
-  let rec nf_fix c =
-    match kind_of_term c with
-        Evar(i,[|fx;f|] as ev) when Evar.Map.mem i minargs ->
-          (match Evd.existential_opt_value sigma' ev with
-              Some c' -> c'
-            | None -> f)
-      | _ -> map_constr nf_fix c in
-  EConstr.of_constr (nf_fix (EConstr.Unsafe.to_constr body))
+  let rec nf_fix c = match EConstr.kind sigma c with
+  | Evar (i,[|fx;f|]) when Evar.Map.mem i minargs ->
+    (** FIXME: find a less hackish way of doing this *)
+    begin match EConstr.kind sigma' c with
+    | Evar _ -> f
+    | c -> EConstr.of_kind c
+    end
+  | _ -> EConstr.map sigma nf_fix c
+  in
+  nf_fix body
 
 type fix_reduction_result = NotReducible | Reduced of (EConstr.t * EConstr.t list)
 
@@ -540,21 +563,21 @@ let match_eval_ref env sigma constr =
       Some (EvalConst sp, u)
   | Var id when is_evaluable env (EvalVarRef id) -> Some (EvalVar id, Univ.Instance.empty)
   | Rel i -> Some (EvalRel i, Univ.Instance.empty)
-  | Evar (evk, args) -> Some (EvalEvar (evk, Array.map EConstr.Unsafe.to_constr args), Univ.Instance.empty)
+  | Evar ev -> Some (EvalEvar ev, Univ.Instance.empty)
   | _ -> None
 
 let match_eval_ref_value env sigma constr = 
-  match kind_of_term constr with
+  match EConstr.kind sigma constr with
   | Const (sp, u) when is_evaluable env (EvalConstRef sp) ->
-    Some (constant_value_in env (sp, u))
+    Some (EConstr.of_constr (constant_value_in env (sp, u)))
   | Var id when is_evaluable env (EvalVarRef id) -> 
-     env |> lookup_named id |> NamedDecl.get_value
+     env |> lookup_named id |> NamedDecl.get_value |> Option.map EConstr.of_constr
   | Rel n ->
-     env |> lookup_rel n |> RelDecl.map_value (lift n) |> RelDecl.get_value
-  | Evar ev -> Evd.existential_opt_value sigma ev
+     env |> lookup_rel n |> RelDecl.map_value (lift n) |> RelDecl.get_value |> Option.map EConstr.of_constr
   | _ -> None
 
 let special_red_case env sigma whfun (ci, p, c, lf) =
+  let open EConstr in
   let rec redrec s =
     let (constr, cargs) = whfun s in
     match match_eval_ref env sigma constr with
@@ -562,13 +585,12 @@ let special_red_case env sigma whfun (ci, p, c, lf) =
       (match reference_opt_value env sigma ref u with
       | None -> raise Redelimination
       | Some gvalue ->
-        let gvalue = EConstr.of_constr gvalue in
         if reducible_mind_case sigma gvalue then
 	  reduce_mind_case_use_function constr env sigma
 	  {mP=p; mconstr=gvalue; mcargs=cargs;
            mci=ci; mlf=lf}
 	else
-	  redrec (EConstr.applist(gvalue, cargs)))
+	  redrec (applist(gvalue, cargs)))
     | None ->
       if reducible_mind_case sigma constr then
         reduce_mind_case sigma
@@ -688,11 +710,11 @@ let rec red_elim_const env sigma ref u largs =
     | EliminationMutualFix (min,refgoal,refinfos) when nargs >= min ->
 	let rec descend (ref,u) args =
 	  let c = reference_value env sigma ref u in
-	  if evaluable_reference_eq ref refgoal then
+	  if evaluable_reference_eq sigma ref refgoal then
 	    (c,args)
 	  else
 	    let c', lrest = whd_betalet_stack sigma (applist(c,args)) in
-	    descend (destEvalRefU (EConstr.Unsafe.to_constr c')) lrest in
+	    descend (destEvalRefU sigma c') lrest in
 	let (_, midargs as s) = descend (ref,u) largs in
 	let d, lrest = whd_nothing_for_iota env sigma (applist s) in
 	let f = make_elim_fun refinfos u midargs in
@@ -803,7 +825,7 @@ and whd_construct_stack env sigma s =
   | Some (ref, u) ->
     (match reference_opt_value env sigma ref u with
     | None -> raise Redelimination
-    | Some gvalue -> whd_construct_stack env sigma (applist(EConstr.of_constr gvalue, cargs)))
+    | Some gvalue -> whd_construct_stack env sigma (applist(gvalue, cargs)))
   | _ -> raise Redelimination
 
 (************************************************************************)
@@ -816,7 +838,6 @@ 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 inj = EConstr.Unsafe.to_constr in
   let open EConstr in
   let rec redrec env x =
     let x = EConstr.of_constr (whd_betaiota sigma x) in
@@ -834,8 +855,7 @@ let try_red_product env sigma c =
              | _ -> simpfun (mkApp (redrec env f, l)))
       | Cast (c,_,_) -> redrec env c
       | Prod (x,a,b) ->
-          let open Context.Rel.Declaration in
-	  mkProd (x, a, redrec (push_rel (LocalAssum (x, inj a)) env) b)
+	  mkProd (x, a, redrec (push_rel (local_assum (x, a)) env) b)
       | LetIn (x,a,b,t) -> redrec env (Vars.subst1 a t)
       | Case (ci,p,d,lf) -> simpfun (mkCase (ci,p,redrec env d,lf))
       | Proj (p, c) -> 
@@ -855,7 +875,7 @@ let try_red_product env sigma c =
           (* to get true one-step reductions *)
 	  (match reference_opt_value env sigma ref u with
 	     | None -> raise Redelimination
-	     | Some c -> EConstr.of_constr c)
+	     | Some c -> c)
 	| _ -> raise Redelimination)
   in EConstr.Unsafe.to_constr (redrec env c)
 
@@ -931,9 +951,9 @@ let whd_simpl_orelse_delta_but_fix env sigma c =
   let open EConstr in
   let rec redrec s =
     let (constr, stack as s') = whd_simpl_stack env sigma s in
-    match match_eval_ref_value env sigma (EConstr.Unsafe.to_constr constr) with
+    match match_eval_ref_value env sigma constr with
     | Some c ->
-      (match kind_of_term (strip_lam c) with
+      (match EConstr.kind sigma (snd (decompose_lam sigma c)) with
       | CoFix _ | Fix _ -> s'
       | Proj (p,t) when
 	  (match EConstr.kind sigma constr with
@@ -943,8 +963,8 @@ let whd_simpl_orelse_delta_but_fix env sigma c =
 	  if List.length stack <= pb.Declarations.proj_npars then
 	    (** Do not show the eta-expanded form *)
 	    s'
-	  else redrec (applist (EConstr.of_constr c, stack))
-      | _ -> redrec (applist(EConstr.of_constr c, stack)))
+	  else redrec (applist (c, stack))
+      | _ -> redrec (applist(c, stack)))
     | None -> s'
   in
   let simpfun = clos_norm_flags betaiota env sigma in
@@ -973,22 +993,25 @@ let matches_head env sigma c t =
     of the projection and its eta expanded form.
 *)
 let change_map_constr_with_binders_left_to_right g f (env, l as acc) sigma c = 
-  match kind_of_term c with
+  let open EConstr in
+  match EConstr.kind sigma c with
   | Proj (p, r) -> (* Treat specially for partial applications *)
-    let t = Retyping.expand_projection env sigma p (EConstr.of_constr r) [] in
-    let hdf, al = destApp t in
+    let t = Retyping.expand_projection env sigma p r [] in
+    let t = EConstr.of_constr t in
+    let hdf, al = destApp sigma t in
     let a = al.(Array.length al - 1) in
     let app = (mkApp (hdf, Array.sub al 0 (Array.length al - 1))) in
     let app' = f acc app in
     let a' = f acc a in
-      (match kind_of_term app' with
+      (match EConstr.kind sigma app' with
       | App (hdf', al') when hdf' == hdf ->
         (* Still the same projection, we ignore the change in parameters *)
 	mkProj (p, a')
       | _ -> mkApp (app', [| a' |]))
-  | _ -> map_constr_with_binders_left_to_right g f acc c
+  | _ -> map_constr_with_binders_left_to_right sigma g f acc c
 
 let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t ->
+  let open EConstr in
   let (nowhere_except_in,locs) = Locusops.convert_occs occs in
   let maxocc = List.fold_right max locs 0 in
   let pos = ref 1 in
@@ -1000,8 +1023,8 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t ->
     else
     try
       let subst =
-        if byhead then matches_head env sigma c (EConstr.of_constr t) 
-	else Constr_matching.matches env sigma c (EConstr.of_constr t) in
+        if byhead then matches_head env sigma c t 
+	else Constr_matching.matches env sigma c t in
       let ok =
 	if nowhere_except_in then Int.List.mem !pos locs
 	else not (Int.List.mem !pos locs) in
@@ -1012,8 +1035,8 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t ->
         (* Skip inner occurrences for stable counting of occurrences *)
         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) (EConstr.of_constr t) in
-	(evd := Sigma.to_evar_map evm; 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)
       end
       else
 	traverse_below nested envc t
@@ -1022,7 +1045,7 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t ->
   and traverse_below nested envc t =
     (* when byhead, find other occurrences without matching again partial
        application with same head *)
-    match kind_of_term t with
+    match EConstr.kind !evd t with
     | App (f,l) when byhead -> mkApp (f, Array.map_left (traverse nested envc) l)
     | Proj (p,c) when byhead -> mkProj (p,traverse nested envc c)
     | _ ->
@@ -1030,9 +1053,9 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t ->
           (fun d (env,c) -> (push_rel d env,lift_pattern 1 c))
           (traverse nested) envc sigma t
   in
-  let t' = traverse None (env,c) (EConstr.Unsafe.to_constr 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 (t', !evd)
+  Sigma.Unsafe.of_pair (EConstr.Unsafe.to_constr t', !evd)
   end }
 
 let contextually byhead occs f env sigma t =
@@ -1068,10 +1091,9 @@ let substlin env sigma evalref n (nowhere_except_in,locs) c =
 	  incr pos;
 	  if ok then value u else c
       | None -> 
-        let self () c = EConstr.Unsafe.to_constr (substrec () (EConstr.of_constr c)) in
-        EConstr.of_constr (map_constr_with_binders_left_to_right
+        map_constr_with_binders_left_to_right sigma
 	  (fun _ () -> ())
-          self () (EConstr.Unsafe.to_constr c))
+          substrec () c
   in
   let t' = substrec () c in
   (!pos, t')
@@ -1082,9 +1104,9 @@ let string_of_evaluable_ref env = function
       string_of_qualid
         (Nametab.shortest_qualid_of_global (vars_of_env env) (ConstRef kn))
 
-let unfold env sigma name =
+let unfold env sigma name c =
   if is_evaluable env name then
-    clos_norm_flags (unfold_red name) env sigma
+    EConstr.of_constr (clos_norm_flags (unfold_red name) env sigma c)
   else
     error (string_of_evaluable_ref env name^" is opaque.")
 
@@ -1102,37 +1124,40 @@ let unfoldoccs env sigma (occs,name) c =
     | [] -> ()
     | _ -> error_invalid_occurrence rest
     in
-    nf_betaiotazeta sigma uc
+    EConstr.of_constr (nf_betaiotazeta sigma uc)
   in
   match occs with
-    | NoOccurrences -> EConstr.Unsafe.to_constr c
+    | NoOccurrences -> c
     | AllOccurrences -> unfold env sigma name c
     | OnlyOccurrences l -> unfo true l
     | AllOccurrencesBut l -> unfo false l
 
 (* Unfold reduction tactic: *)
 let unfoldn loccname env sigma c =
-  EConstr.Unsafe.to_constr (List.fold_left (fun c occname -> EConstr.of_constr (unfoldoccs env sigma occname c)) c loccname)
+  EConstr.Unsafe.to_constr (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 open EConstr in
   let rcom =
-    try red_product env sigma (EConstr.of_constr com)
+    try EConstr.of_constr (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 (EConstr.of_constr rcom))) c in
-  if not (eq_constr a (EConstr.Unsafe.to_constr c)) then
-    subst1 com a
+  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 (EConstr.of_constr rcom) c in
-    subst1 com a
+    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 =
-  EConstr.Unsafe.to_constr (List.fold_right (fun com c -> EConstr.of_constr (fold_one_com com env sigma c)) (List.rev cl) c)
+  EConstr.Unsafe.to_constr (List.fold_right (fun com c -> fold_one_com com env sigma c) (List.rev cl) c)
 
 
 (* call by value reduction functions *)
@@ -1150,23 +1175,26 @@ let compute = cbv_betadeltaiota
 (* gives [na:ta]c' such that c converts to ([na:ta]c' a), abstracting only
  * the specified occurrences. *)
 
-let abstract_scheme env (locc,a) (c, sigma) =
-  let a = EConstr.of_constr a in
+let abstract_scheme env sigma (locc,a) (c, sigma) =
+  let open EConstr in
   let ta = Retyping.get_type_of env sigma a in
-  let na = named_hd env ta Anonymous in
-  if occur_meta sigma (EConstr.of_constr ta) then error "Cannot find a type for the generalisation.";
+  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
     mkLambda (na,ta,c), sigma
   else
-    let c', sigma' = subst_closed_term_occ env sigma (AtOccs locc) a (EConstr.of_constr c) in
+    let c', sigma' = subst_closed_term_occ env sigma (AtOccs locc) a c in
+    let c' = EConstr.of_constr c' in
       mkLambda (na,ta,c'), sigma'
 
 let pattern_occs loccs_trm = { e_redfun = begin fun env sigma c ->
+  let open EConstr in
   let sigma = Sigma.to_evar_map sigma in
-  let abstr_trm, sigma = List.fold_right (abstract_scheme env) loccs_trm (EConstr.Unsafe.to_constr c,sigma) in
+  let abstr_trm, sigma = List.fold_right (abstract_scheme env sigma) loccs_trm (c,sigma) in
   try
-    let _ = Typing.unsafe_type_of env sigma (EConstr.of_constr abstr_trm) in
-    Sigma.Unsafe.of_pair (applist(abstr_trm, List.map snd loccs_trm), sigma)
+    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)
   with Type_errors.TypeError (env',t) ->
     raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t))))
   end }
@@ -1190,28 +1218,31 @@ let check_not_primitive_record env ind =
    return name, B and t' *)
 
 let reduce_to_ind_gen allow_product env sigma t =
+  let open EConstr in
   let rec elimrec env t l =
-    let t = hnf_constr env sigma (EConstr.of_constr t) in
-    match kind_of_term (fst (decompose_app t)) with
-      | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn 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
+      | Ind ind-> (check_privacy env ind, EConstr.Unsafe.to_constr (it_mkProd_or_LetIn t l))
       | Prod (n,ty,t') ->
 	  let open Context.Rel.Declaration in
 	  if allow_product then
-	    elimrec (push_rel (LocalAssum (n,ty)) env) t' ((LocalAssum (n,ty))::l)
+	    elimrec (push_rel (local_assum (n,ty)) env) t' ((local_assum (n,ty))::l)
 	  else
 	    user_err  (str"Not an inductive definition.")
       | _ ->
 	  (* 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 (EConstr.of_constr t) in
-	  match kind_of_term (fst (decompose_app t')) with
-	    | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t' l)
+	  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
+	    | Ind ind-> (check_privacy env ind, EConstr.Unsafe.to_constr (it_mkProd_or_LetIn t' l))
 	    | _ -> user_err  (str"Not an inductive product.")
   in
   elimrec env t []
 
-let reduce_to_quantified_ind x = reduce_to_ind_gen true x
-let reduce_to_atomic_ind x = reduce_to_ind_gen false x
+let reduce_to_quantified_ind env sigma c = reduce_to_ind_gen true env sigma (EConstr.of_constr c)
+let reduce_to_atomic_ind env sigma c = reduce_to_ind_gen false env sigma (EConstr.of_constr c)
 
 let find_hnf_rectype env sigma t =
   let ind,t = reduce_to_atomic_ind env sigma t in
@@ -1243,13 +1274,13 @@ let one_step_reduce env sigma c =
              | Reduced s' -> s'
 	     | NotReducible -> raise NotStepReducible
            with Redelimination -> raise NotStepReducible)
-      | _ when isEvalRef env (EConstr.Unsafe.to_constr x) ->
-	  let ref,u = destEvalRefU (EConstr.Unsafe.to_constr x) in
+      | _ when isEvalRef env sigma x ->
+	  let ref,u = destEvalRefU sigma x in
           (try
              fst (red_elim_const env sigma ref u stack)
            with Redelimination ->
 	     match reference_opt_value env sigma ref u with
-	       | Some d -> (EConstr.of_constr d, stack)
+	       | Some d -> (d, stack)
 	       | None -> raise NotStepReducible)
 
       | _ -> raise NotStepReducible
@@ -1271,26 +1302,29 @@ let reduce_to_ref_gen allow_product env sigma ref t =
   else
   (* lazily reduces to match the head of [t] with the expected [ref] *)
   let rec elimrec env t l =
-    let c, _ = decompose_app_vect sigma (EConstr.of_constr t) in
-    match kind_of_term c with
+    let open EConstr in
+    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
 	    let open Context.Rel.Declaration in
-	    elimrec (push_rel (LocalAssum (n,t)) env) t' ((LocalAssum (n,ty))::l)
+	    elimrec (push_rel (local_assum (n,t)) env) t' ((local_assum (n,ty))::l)
           else
             error_cannot_recognize ref
       | _ ->
 	  try
-	    if eq_gr (global_of_constr c) ref
+	    if eq_gr (global_of_constr (EConstr.to_constr sigma c)) ref
 	    then it_mkProd_or_LetIn t l
 	    else raise Not_found
 	  with Not_found ->
           try
-	    let t' = nf_betaiota sigma (one_step_reduce env sigma (EConstr.of_constr t)) in
+	    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
-  elimrec env t []
+  EConstr.Unsafe.to_constr (elimrec env t [])
 
 let reduce_to_quantified_ref = reduce_to_ref_gen true
 let reduce_to_atomic_ref = reduce_to_ref_gen false
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index f8dfe1adf..d32fcf491 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -17,7 +17,7 @@ open Locus
 open Univ
 
 type reduction_tactic_error =
-    InvalidAbstraction of env * evar_map * constr * (env * Type_errors.type_error)
+    InvalidAbstraction of env * evar_map * EConstr.constr * (env * Type_errors.type_error)
 
 exception ReductionTacticError of reduction_tactic_error
 
@@ -58,10 +58,10 @@ val unfoldn :
   (occurrences * evaluable_global_reference) list ->  reduction_function
 
 (** Fold *)
-val fold_commands : constr list ->  reduction_function
+val fold_commands : EConstr.constr list ->  reduction_function
 
 (** Pattern *)
-val pattern_occs : (occurrences * constr) list -> e_reduction_function
+val pattern_occs : (occurrences * EConstr.constr) list -> e_reduction_function
 
 (** Rem: Lazy strategies are defined in Reduction *)
 
@@ -85,10 +85,10 @@ val reduce_to_quantified_ind : env ->  evar_map -> types -> pinductive * types
 (** [reduce_to_quantified_ref env sigma ref t] try to put [t] in the form
    [t'=(x1:A1)..(xn:An)(ref args)] and fails with user error if not possible *)
 val reduce_to_quantified_ref :
-  env ->  evar_map -> global_reference -> types -> types
+  env ->  evar_map -> global_reference -> EConstr.types -> types
 
 val reduce_to_atomic_ref :
-  env ->  evar_map -> global_reference -> types -> types
+  env ->  evar_map -> global_reference -> EConstr.types -> types
 
 val find_hnf_rectype : 
   env ->  evar_map -> types -> pinductive * constr list
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index f418dc6a9..786cfd31f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1611,7 +1611,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
         (push_named_context_val d sign,depdecls)
     | AllOccurrences, InHyp as occ ->
         let occ = if likefirst then LikeFirst else AtOccs occ in
-        let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in
+        let newdecl = replace_term_occ_decl_modulo sigma occ test mkvarid d in
         if Context.Named.Declaration.equal d newdecl
            && not (indirectly_dependent sigma c d depdecls)
         then
@@ -1622,7 +1622,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
           (push_named_context_val newdecl sign, newdecl :: depdecls)
     | occ ->
         (* There are specific occurrences, hence not like first *)
-        let newdecl = replace_term_occ_decl_modulo (AtOccs occ) test mkvarid d in
+        let newdecl = replace_term_occ_decl_modulo sigma (AtOccs occ) test mkvarid d in
         (push_named_context_val newdecl sign, newdecl :: depdecls) in
   try
     let sign,depdecls =
@@ -1632,7 +1632,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
       | NoOccurrences -> concl
       | occ ->
           let occ = if likefirst then LikeFirst else AtOccs occ in
-          replace_term_occ_modulo occ test mkvarid (EConstr.of_constr concl)
+          replace_term_occ_modulo sigma occ test mkvarid (EConstr.of_constr concl)
     in
     let lastlhyp =
       if List.is_empty depdecls then None else Some (NamedDecl.get_id (List.last depdecls)) in
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 19e72e697..d4a58da32 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -200,6 +200,9 @@ let out_arg = function
 let out_with_occurrences (occs,c) =
   (Locusops.occurrences_map (List.map out_arg) occs, c)
 
+let out_with_occurrences' (occs,c) =
+  (Locusops.occurrences_map (List.map out_arg) occs, EConstr.of_constr c)
+
 let e_red f = { e_redfun = fun env evm c -> Sigma.here (f env (Sigma.to_evar_map evm) c) evm }
 
 let head_style = false (* Turn to true to have a semantics where simpl
@@ -239,8 +242,8 @@ let reduction_of_red_expr env =
      (e_red (strong_cbn (make_flag f)), DEFAULTcast)
   | Lazy f -> (e_red (clos_norm_flags (make_flag f)),DEFAULTcast)
   | Unfold ubinds -> (e_red (unfoldn (List.map out_with_occurrences ubinds)),DEFAULTcast)
-  | Fold cl -> (e_red (fold_commands cl),DEFAULTcast)
-  | Pattern lp -> (pattern_occs (List.map out_with_occurrences lp),DEFAULTcast)
+  | Fold cl -> (e_red (fold_commands (List.map EConstr.of_constr cl)),DEFAULTcast)
+  | Pattern lp -> (pattern_occs (List.map out_with_occurrences' lp),DEFAULTcast)
   | ExtraRedExpr s ->
       (try (e_red (String.Map.find s !reduction_tab),DEFAULTcast)
       with Not_found ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8fb47b994..e4503dab6 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -875,7 +875,7 @@ let normalise_vm_in_concl = reduct_in_concl (Redexpr.cbv_vm,VMcast)
 let unfold_in_concl loccname = reduct_in_concl (unfoldn loccname,REVERTcast)
 let unfold_in_hyp   loccname = reduct_in_hyp   (unfoldn loccname)
 let unfold_option   loccname = reduct_option (unfoldn loccname,DEFAULTcast)
-let pattern_option l = e_reduct_option (pattern_occs l,DEFAULTcast)
+let pattern_option l = e_reduct_option (pattern_occs (List.map (on_snd EConstr.of_constr) l),DEFAULTcast)
 
 (* The main reduction function *)
 
@@ -3165,7 +3165,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
   let env = Proofview.Goal.env gl in
   let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 (Proofview.Goal.assume gl) in
   let reduce_to_quantified_ref = Tacmach.New.pf_apply reduce_to_quantified_ref gl in
-  let typ0 = reduce_to_quantified_ref indref tmptyp0 in
+  let typ0 = reduce_to_quantified_ref indref (EConstr.of_constr tmptyp0) in
   let prods, indtyp = decompose_prod_assum typ0 in
   let hd,argl = decompose_app indtyp in
   let env' = push_rel_context prods env in
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index b480fcd86..1d82d9ae1 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1270,6 +1270,7 @@ let explain_pattern_matching_error env sigma = function
 
 let explain_reduction_tactic_error = function
   | Tacred.InvalidAbstraction (env,sigma,c,(env',e)) ->
+      let c = EConstr.to_constr sigma c in
       str "The abstracted term" ++ spc () ++
       quote (pr_goal_concl_style_env env sigma c) ++
       spc () ++ str "is not well typed." ++ fnl () ++