Termops API using EConstr.

15 files changed, 190 insertions, 183 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index d5b125135..6b480986c 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -535,19 +535,19 @@ let dependencies_in_pure_rhs nargs eqns =
   let deps_columns = matrix_transpose deps_rows in
   List.map (List.exists (fun x -> x)) deps_columns
 
-let dependent_decl a =
+let dependent_decl sigma a =
   function
-  | LocalAssum (na,t) -> dependent a t
-  | LocalDef (na,c,t) -> dependent a t || dependent a c
+  | LocalAssum (na,t) -> dependent sigma (EConstr.of_constr a) (EConstr.of_constr t)
+  | LocalDef (na,c,t) -> dependent sigma (EConstr.of_constr a) (EConstr.of_constr t) || dependent sigma (EConstr.of_constr a) (EConstr.of_constr c)
 
-let rec dep_in_tomatch n = function
-  | (Pushed _ | Alias _ | NonDepAlias) :: l -> dep_in_tomatch n l
-  | Abstract (_,d) :: l -> dependent_decl (mkRel n) d || dep_in_tomatch (n+1) l
+let rec dep_in_tomatch sigma n = function
+  | (Pushed _ | Alias _ | NonDepAlias) :: l -> dep_in_tomatch sigma n l
+  | Abstract (_,d) :: l -> dependent_decl sigma (mkRel n) d || dep_in_tomatch sigma (n+1) l
   | [] -> false
 
-let dependencies_in_rhs nargs current tms eqns =
+let dependencies_in_rhs sigma nargs current tms eqns =
   match kind_of_term current with
-  | Rel n when dep_in_tomatch n tms -> List.make nargs true
+  | Rel n when dep_in_tomatch sigma n tms -> List.make nargs true
   | _ -> dependencies_in_pure_rhs nargs eqns
 
 (* Computing the matrix of dependencies *)
@@ -562,24 +562,24 @@ let dependencies_in_rhs nargs current tms eqns =
    [n-2;1], [1] points to [dn] and [n-2] to [d3]
 *)
 
-let rec find_dependency_list tmblock = function
+let rec find_dependency_list sigma tmblock = function
   | [] -> []
   | (used,tdeps,d)::rest ->
-      let deps = find_dependency_list tmblock rest in
-      if used && List.exists (fun x -> dependent_decl x d) tmblock
+      let deps = find_dependency_list sigma tmblock rest in
+      if used && List.exists (fun x -> dependent_decl sigma x d) tmblock
       then
         List.add_set Int.equal
           (List.length rest + 1) (List.union Int.equal deps tdeps)
       else deps
 
-let find_dependencies is_dep_or_cstr_in_rhs (tm,(_,tmtypleaves),d) nextlist =
-  let deps = find_dependency_list (tm::tmtypleaves) nextlist in
+let find_dependencies sigma is_dep_or_cstr_in_rhs (tm,(_,tmtypleaves),d) nextlist =
+  let deps = find_dependency_list sigma (tm::tmtypleaves) nextlist in
   if is_dep_or_cstr_in_rhs || not (List.is_empty deps)
   then ((true ,deps,d)::nextlist)
   else ((false,[]  ,d)::nextlist)
 
-let find_dependencies_signature deps_in_rhs typs =
-  let l = List.fold_right2 find_dependencies deps_in_rhs typs [] in
+let find_dependencies_signature sigma deps_in_rhs typs =
+  let l = List.fold_right2 (find_dependencies sigma) deps_in_rhs typs [] in
   List.map (fun (_,deps,_) -> deps) l
 
 (* Assume we had terms t1..tq to match in a context xp:Tp,...,x1:T1 |-
@@ -1095,30 +1095,30 @@ let rec ungeneralize n ng body =
 let ungeneralize_branch n k (sign,body) cs =
   (sign,ungeneralize (n+cs.cs_nargs) k body)
 
-let rec is_dependent_generalization ng body =
+let rec is_dependent_generalization sigma ng body =
   match kind_of_term body with
   | Lambda (_,_,c) when Int.equal ng 0 ->
-      dependent (mkRel 1) c
+      not (EConstr.Vars.noccurn sigma 1 (EConstr.of_constr c))
   | Lambda (na,t,c) ->
       (* We traverse an inner generalization *)
-      is_dependent_generalization (ng-1) c
+      is_dependent_generalization sigma (ng-1) c
   | LetIn (na,b,t,c) ->
       (* We traverse an alias *)
-      is_dependent_generalization ng c
+      is_dependent_generalization sigma ng c
   | Case (ci,p,c,brs) ->
       (* We traverse a split *)
       Array.exists2 (fun q c ->
         let _,b = decompose_lam_n_decls q c in
-        is_dependent_generalization ng b)
+        is_dependent_generalization sigma ng b)
         ci.ci_cstr_ndecls brs
   | App (g,args) ->
       (* We traverse an inner generalization *)
       assert (isCase g);
-      is_dependent_generalization (ng+Array.length args) g
+      is_dependent_generalization sigma (ng+Array.length args) g
   | _ -> assert false
 
-let is_dependent_branch k (_,br) =
-  is_dependent_generalization k br
+let is_dependent_branch sigma k (_,br) =
+  is_dependent_generalization sigma k br
 
 let postprocess_dependencies evd tocheck brs tomatch pred deps cs =
   let rec aux k brs tomatch pred tocheck deps = match deps, tomatch with
@@ -1126,8 +1126,8 @@ let postprocess_dependencies evd tocheck brs tomatch pred deps cs =
   | n::deps, Abstract (i,d) :: tomatch ->
       let d = map_constr (nf_evar evd) d in
       let is_d = match d with LocalAssum _ -> false | LocalDef _ -> true in
-      if is_d || List.exists (fun c -> dependent_decl (lift k c) d) tocheck
-                 && Array.exists (is_dependent_branch k) brs then
+      if is_d || List.exists (fun c -> dependent_decl evd (lift k c) d) tocheck
+                 && Array.exists (is_dependent_branch evd k) brs then
         (* Dependency in the current term to match and its dependencies is real *)
         let brs,tomatch,pred,inst = aux (k+1) brs tomatch pred (mkRel n::tocheck) deps in
         let inst = match d with
@@ -1249,8 +1249,8 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
   (* We compute over which of x(i+1)..xn and x matching on xi will need a *)
   (* generalization *)
   let dep_sign =
-    find_dependencies_signature
-      (dependencies_in_rhs const_info.cs_nargs current pb.tomatch eqns)
+    find_dependencies_signature !(pb.evdref)
+      (dependencies_in_rhs !(pb.evdref) const_info.cs_nargs current pb.tomatch eqns)
       (List.rev typs') in
 
   (* The dependent term to subst in the types of the remaining UnPushed
@@ -1452,7 +1452,7 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest =
          mat = List.map (push_alias_eqn alias) pb.mat } in
     let j = compile pb in
     { uj_val =
-        if isRel c || isVar c || count_occurrences (mkRel 1) j.uj_val <= 1 then
+        if isRel c || isVar c || count_occurrences !(pb.evdref) (EConstr.mkRel 1) (EConstr.of_constr j.uj_val) <= 1 then
           subst1 c j.uj_val
         else
           mkLetIn (na,c,t,j.uj_val);
@@ -1561,7 +1561,7 @@ let matx_of_eqns env eqns =
    returning True never happens and any inhabited type can be put instead).
 *)
 
-let adjust_to_extended_env_and_remove_deps env extenv subst t =
+let adjust_to_extended_env_and_remove_deps env extenv sigma subst t =
   let n = Context.Rel.length (rel_context env) in
   let n' = Context.Rel.length (rel_context extenv) in
   (* We first remove the bindings that are dependently typed (they are
@@ -1583,7 +1583,7 @@ let adjust_to_extended_env_and_remove_deps env extenv subst t =
       | LocalAssum _ -> p in
     let p = traverse_local_defs p in
     let u = lift (n' - n) u in
-    try Some (p, u, expand_vars_in_term extenv u)
+    try Some (p, u, expand_vars_in_term extenv sigma u)
       (* pedrot: does this really happen to raise [Failure _]? *)
     with Failure _ -> None in
   let subst0 = List.map_filter map subst in
@@ -1617,7 +1617,7 @@ let abstract_tycon loc env evdref subst tycon extenv t =
   let src = match kind_of_term t with
     | Evar (evk,_) -> (loc,Evar_kinds.SubEvar evk)
     | _ -> (loc,Evar_kinds.CasesType true) in
-  let subst0,t0 = adjust_to_extended_env_and_remove_deps env extenv subst t in
+  let subst0,t0 = adjust_to_extended_env_and_remove_deps env extenv !evdref subst t in
   (* We traverse the type T of the original problem Xi looking for subterms
      that match the non-constructor part of the constraints (this part
      is in subst); these subterms are the "good" subterms and we replace them
@@ -1644,7 +1644,8 @@ let abstract_tycon loc env evdref subst tycon extenv t =
     let good = List.filter (fun (_,u,_) -> is_conv_leq env !evdref t u) subst in
     match good with
     | [] ->
-      map_constr_with_full_binders push_binder aux x t
+      let self env c = EConstr.of_constr (aux env (EConstr.Unsafe.to_constr c)) in
+      EConstr.Unsafe.to_constr (map_constr_with_full_binders !evdref push_binder self x (EConstr.of_constr t))
     | (_, _, u) :: _ -> (* u is in extenv *)
       let vl = List.map pi1 good in
       let ty = 
@@ -1652,16 +1653,16 @@ let abstract_tycon loc env evdref subst tycon extenv t =
 	  Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty
       in
       let ty = lift (-k) (aux x ty) in
-      let depvl = free_rels ty in
+      let depvl = free_rels !evdref (EConstr.of_constr ty) in
       let inst =
 	List.map_i
 	  (fun i _ -> if Int.List.mem i vl then u else mkRel i) 1
 	  (rel_context extenv) in
       let rel_filter =
-	List.map (fun a -> not (isRel a) || dependent a u
+	List.map (fun a -> not (isRel a) || dependent !evdref (EConstr.of_constr a) (EConstr.of_constr u)
                            || Int.Set.mem (destRel a) depvl) inst in
       let named_filter =
-	List.map (fun d -> dependent (mkVar (NamedDecl.get_id d)) u)
+	List.map (fun d -> local_occur_var !evdref (NamedDecl.get_id d) (EConstr.of_constr u))
 	  (named_context extenv) in
       let filter = Filter.make (rel_filter @ named_filter) in
       let candidates = u :: List.map mkRel vl in
@@ -1753,7 +1754,7 @@ let build_inversion_problem loc env sigma tms t =
     List.map (fun (c,d) -> (c,extract_inductive_data pb_env sigma d,d)) decls in
 
   let decls = List.rev decls in
-  let dep_sign = find_dependencies_signature (List.make n true) decls in
+  let dep_sign = find_dependencies_signature sigma (List.make n true) decls in
 
   let sub_tms =
     List.map2 (fun deps (tm, (tmtyp,_), decl) ->
@@ -1878,7 +1879,7 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
     List.fold_right2 (fun (tm, tmtype) sign (subst, len) ->
       let signlen = List.length sign in
 	match kind_of_term tm with
-	  | Rel n when dependent tm c
+	  | Rel n when dependent sigma (EConstr.of_constr tm) (EConstr.of_constr c)
 		&& Int.equal signlen 1 (* The term to match is not of a dependent type itself *) ->
 	      ((n, len) :: subst, len - signlen)
 	  | Rel n when signlen > 1 (* The term is of a dependent type,
@@ -1890,13 +1891,13 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
 		      List.fold_left
 			(fun (subst, len) arg ->
 			  match kind_of_term arg with
-			  | Rel n when dependent arg c ->
+			  | Rel n when dependent sigma (EConstr.of_constr arg) (EConstr.of_constr c) ->
 			      ((n, len) :: subst, pred len)
 			  | _ -> (subst, pred len))
 			(subst, len) realargs
 		    in
 		    let subst =
-		      if dependent tm c && List.for_all isRel realargs
+		      if dependent sigma (EConstr.of_constr tm) (EConstr.of_constr c) && List.for_all isRel realargs
 		      then (n, len) :: subst else subst
 		    in (subst, pred len))
 	  | _ -> (subst, len - signlen))
@@ -2279,7 +2280,7 @@ let lift_ctx n ctx =
   in ctx'
 
 (* Turn matched terms into variables. *)
-let abstract_tomatch env tomatchs tycon =
+let abstract_tomatch env sigma tomatchs tycon =
   let prev, ctx, names, tycon =
     List.fold_left
       (fun (prev, ctx, names, tycon) (c, t) ->
@@ -2288,7 +2289,7 @@ let abstract_tomatch env tomatchs tycon =
 	     Rel n -> (lift lenctx c, lift_tomatch_type lenctx t) :: prev, ctx, names, tycon
 	   | _ ->
 	       let tycon = Option.map
-		 (fun t -> subst_term (lift 1 c) (lift 1 t)) tycon in
+		 (fun t -> subst_term sigma (EConstr.of_constr (lift 1 c)) (EConstr.of_constr (lift 1 t))) tycon in
 	       let name = next_ident_away (Id.of_string "filtered_var") names in
 		 (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev,
 	       LocalDef (Name name, lift lenctx c, lift lenctx $ type_of_tomatch t) :: ctx,
@@ -2406,7 +2407,7 @@ let compile_program_cases loc style (typing_function, evdref) tycon env
   (* constructors found in patterns *)
   let tomatchs = coerce_to_indtype typing_function evdref env matx tomatchl in
   let tycon = valcon_of_tycon tycon in
-  let tomatchs, tomatchs_lets, tycon' = abstract_tomatch env tomatchs tycon in
+  let tomatchs, tomatchs_lets, tycon' = abstract_tomatch env !evdref tomatchs tycon in
   let env = push_rel_context tomatchs_lets env in
   let len = List.length eqns in
   let sign, allnames, signlen, eqs, neqs, args =
@@ -2460,7 +2461,7 @@ let compile_program_cases loc style (typing_function, evdref) tycon env
     List.map (fun (c,d) -> (c,extract_inductive_data env !evdref d,d)) typs in
     
   let dep_sign =
-    find_dependencies_signature
+    find_dependencies_signature !evdref
       (List.make (List.length typs) true)
       typs in
     
@@ -2535,7 +2536,7 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e
       List.map (fun (c,d) -> (c,extract_inductive_data env sigma d,d)) typs in
 
     let dep_sign =
-      find_dependencies_signature
+      find_dependencies_signature !evdref
         (List.make (List.length typs) true)
         typs in
 
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 2b860ae9c..a3970fc0f 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -487,7 +487,7 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
           let v1 = Option.get v1 in
 	  let v2 = Option.map (fun v -> beta_applist (lift 1 v,[v1])) v in
 	  let t2 = match v2 with
-	    | None -> subst_term v1 t2
+	    | None -> subst_term evd' (EConstr.of_constr v1) (EConstr.of_constr t2)
 	    | Some v2 -> Retyping.get_type_of env1 evd' v2 in
 	  let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in
 	    (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2')
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 5ec44a68d..d7b73d333 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -79,7 +79,7 @@ let add_binders na1 na2 binding_vars (names, terms as subst) =
       (names, terms)
   | _ -> subst
 
-let rec build_lambda vars ctx m = match vars with
+let rec build_lambda sigma vars ctx m = match vars with
 | [] ->
   let len = List.length ctx in
   lift (-1 * len) m
@@ -100,12 +100,12 @@ let rec build_lambda vars ctx m = match vars with
     let map i = if i > n then pred i else i in
     let vars = List.map map vars in
     (** Check that the abstraction is legal *)
-    let frels = free_rels t in
+    let frels = free_rels sigma (EConstr.of_constr t) in
     let brels = List.fold_right Int.Set.add vars Int.Set.empty in
     let () = if not (Int.Set.subset frels brels) then raise PatternMatchingFailure in
     (** Create the abstraction *)
     let m = mkLambda (na, t, m) in
-    build_lambda vars (pre @ suf) m
+    build_lambda sigma vars (pre @ suf) m
 
 let rec extract_bound_aux k accu frels ctx = match ctx with
 | [] -> accu
@@ -133,12 +133,12 @@ let make_renaming ids = function
   end
 | _ -> dummy_constr
 
-let merge_binding allow_bound_rels ctx n cT subst =
+let merge_binding sigma allow_bound_rels ctx n cT subst =
   let c = match ctx with
   | [] -> (* Optimization *)
     ([], cT)
   | _ ->
-    let frels = free_rels cT in
+    let frels = free_rels sigma (EConstr.of_constr cT) in
     if allow_bound_rels then
       let vars = extract_bound_vars frels ctx in
       let ordered_vars = Id.Set.elements vars in
@@ -169,7 +169,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
        else false)
   in
   let rec sorec ctx env subst p t =
-    let cT = strip_outer_cast t in
+    let cT = strip_outer_cast sigma (EConstr.of_constr t) in
     match p,kind_of_term cT with
       | PSoApp (n,args),m ->
         let fold (ans, seen) = function
@@ -179,13 +179,13 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
         | _ -> error "Only bound indices allowed in second order pattern matching."
         in
         let relargs, relset = List.fold_left fold ([], Int.Set.empty) args in
-        let frels = free_rels cT in
+        let frels = free_rels sigma (EConstr.of_constr cT) in
         if Int.Set.subset frels relset then
-          constrain n ([], build_lambda relargs ctx cT) subst
+          constrain n ([], build_lambda sigma relargs ctx cT) subst
         else
           raise PatternMatchingFailure
 
-      | PMeta (Some n), m -> merge_binding allow_bound_rels ctx n cT subst
+      | PMeta (Some n), m -> merge_binding sigma allow_bound_rels ctx n cT subst
 
       | PMeta None, m -> subst
 
@@ -216,7 +216,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
             let subst =
               match meta with
               | None -> subst
-              | Some n -> merge_binding allow_bound_rels ctx n c subst in
+              | Some n -> merge_binding sigma allow_bound_rels ctx n c subst in
             Array.fold_left2 (sorec ctx env) subst args1 args22
           else (* Might be a projection on the right *)
 	    match kind_of_term c2 with
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index cad5551c1..72cf31010 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -215,11 +215,11 @@ let lookup_name_as_displayed env t s =
     | Prod (name,_,c') ->
 	(match compute_displayed_name_in RenamingForGoal avoid name c' with
            | (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c'
-	   | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c'))
+	   | (Anonymous,avoid') -> lookup avoid' (n+1) (pop (EConstr.of_constr c')))
     | LetIn (name,_,_,c') ->
 	(match compute_displayed_name_in RenamingForGoal avoid name c' with
            | (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c'
-	   | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c'))
+	   | (Anonymous,avoid') -> lookup avoid' (n+1) (pop (EConstr.of_constr c')))
     | Cast (c,_,_) -> lookup avoid n c
     | _ -> None
   in lookup (ids_of_named_context (named_context env)) 1 t
@@ -261,13 +261,13 @@ let update_name na ((_,(e,_)),c) =
   | _ ->
       na
 
-let rec decomp_branch tags nal b (avoid,env as e) c =
+let rec decomp_branch tags nal b (avoid,env as e) sigma c =
   let flag = if b then RenamingForGoal else RenamingForCasesPattern (fst env,c) in
   match tags with
   | [] -> (List.rev nal,(e,c))
   | b::tags ->
       let na,c,f,body,t =
-        match kind_of_term (strip_outer_cast c), b with
+        match kind_of_term (strip_outer_cast sigma (EConstr.of_constr c)), b with
 	| Lambda (na,t,c),false -> na,c,compute_displayed_let_name_in,None,Some t
 	| LetIn (na,b,t,c),true ->
             na,c,compute_displayed_name_in,Some b,Some t
@@ -279,17 +279,17 @@ let rec decomp_branch tags nal b (avoid,env as e) c =
     in
     let na',avoid' = f flag avoid na c in
     decomp_branch tags (na'::nal) b
-      (avoid', add_name_opt na' body t env) c
+      (avoid', add_name_opt na' body t env) sigma c
 
-let rec build_tree na isgoal e ci cl =
+let rec build_tree na isgoal e sigma ci cl =
   let mkpat n rhs pl = PatCstr(dl,(ci.ci_ind,n+1),pl,update_name na rhs) in
   let cnl = ci.ci_pp_info.cstr_tags in
   let cna = ci.ci_cstr_nargs in
   List.flatten
     (List.init (Array.length cl)
-      (fun i -> contract_branch isgoal e (cnl.(i),cna.(i),mkpat i,cl.(i))))
+      (fun i -> contract_branch isgoal e sigma (cnl.(i),cna.(i),mkpat i,cl.(i))))
 
-and align_tree nal isgoal (e,c as rhs) = match nal with
+and align_tree nal isgoal (e,c as rhs) sigma = match nal with
   | [] -> [[],rhs]
   | na::nal ->
     match kind_of_term c with
@@ -298,20 +298,20 @@ and align_tree nal isgoal (e,c as rhs) = match nal with
         && not (Int.equal (Array.length cl) 0)
 	&& (* don't contract if p dependent *)
 	computable p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) ->
-	let clauses = build_tree na isgoal e ci cl in
+	let clauses = build_tree na isgoal e sigma ci cl in
 	List.flatten
           (List.map (fun (pat,rhs) ->
-	      let lines = align_tree nal isgoal rhs in
+	      let lines = align_tree nal isgoal rhs sigma in
 	      List.map (fun (hd,rest) -> pat::hd,rest) lines)
 	    clauses)
     | _ ->
 	let pat = PatVar(dl,update_name na rhs) in
-	let mat = align_tree nal isgoal rhs in
+	let mat = align_tree nal isgoal rhs sigma in
 	List.map (fun (hd,rest) -> pat::hd,rest) mat
 
-and contract_branch isgoal e (cdn,can,mkpat,b) =
-  let nal,rhs = decomp_branch cdn [] isgoal e b in
-  let mat = align_tree nal isgoal rhs in
+and contract_branch isgoal e sigma (cdn,can,mkpat,b) =
+  let nal,rhs = decomp_branch cdn [] isgoal e sigma b in
+  let mat = align_tree nal isgoal rhs sigma in
   List.map (fun (hd,rhs) -> (mkpat rhs hd,rhs)) mat
 
 (**********************************************************************)
@@ -439,7 +439,7 @@ let detype_instance sigma l =
   else Some (List.map (detype_level sigma) (Array.to_list (Univ.Instance.to_array l)))
 
 let rec detype flags avoid env sigma t =
-  match kind_of_term (collapse_appl t) with
+  match kind_of_term (collapse_appl sigma (EConstr.of_constr t)) with
     | Rel n ->
       (try match lookup_name_of_rel n (fst env) with
 	 | Name id   -> GVar (dl, id)
@@ -628,7 +628,7 @@ and share_names flags n l avoid env sigma c t =
 and detype_eqns flags avoid env sigma ci computable constructs consnargsl bl =
   try
     if !Flags.raw_print || not (reverse_matching ()) then raise Exit;
-    let mat = build_tree Anonymous (snd flags) (avoid,env) ci bl in
+    let mat = build_tree Anonymous (snd flags) (avoid,env) sigma ci bl in
     List.map (fun (pat,((avoid,env),c)) -> (dl,[],[pat],detype flags avoid env sigma c))
       mat
   with e when CErrors.noncritical e ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index d06009dce..194d0b297 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -141,9 +141,10 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
       match kind_of_term t2 with
 	Prod (_,a,b) -> (* assert (l2=[]); *)
 	  let _, a, b = destProd (Evarutil.nf_evar sigma t2) in
-      	  if dependent (mkRel 1) b then raise Not_found
-	  else lookup_canonical_conversion (proji, Prod_cs),
-	    (Stack.append_app [|a;pop b|] Stack.empty)
+          if EConstr.Vars.noccurn sigma 1 (EConstr.of_constr b) then
+            lookup_canonical_conversion (proji, Prod_cs),
+	    (Stack.append_app [|a;pop (EConstr.of_constr b)|] Stack.empty)
+          else raise Not_found
       | Sort s ->
 	lookup_canonical_conversion
 	  (proji, Sort_cs (family_of_sort s)),[]
@@ -178,7 +179,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
   let c' = subst_univs_level_constr subst c in
   let t' = subst_univs_level_constr subst t' in
   let bs' = List.map (subst_univs_level_constr subst) bs in
-  let h, _ = decompose_app_vect t' in
+  let h, _ = decompose_app_vect sigma (EConstr.of_constr t') in
     ctx',(h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1),
     (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1,
     (n,Stack.zip(t2,sk2))
@@ -372,7 +373,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
       | None -> fallback ()
       | Some l1' -> (* Miller-Pfenning's patterns unification *)
 	let t2 = nf_evar evd tM in
-	let t2 = solve_pattern_eqn env l1' t2 in
+	let t2 = solve_pattern_eqn env evd l1' t2 in
 	  solve_simple_eqn (evar_conv_x ts) env evd
 	    (position_problem on_left pbty,ev,t2) 
   in
@@ -893,7 +894,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
        (fun i -> exact_ise_stack2 env i (evar_conv_x trs) sk1 sk2);
        test;
        (fun i -> evar_conv_x trs env i CONV h2
-	 (fst (decompose_app_vect (substl ks h))))]
+	 (fst (decompose_app_vect i (EConstr.of_constr (substl ks h)))))]
   else UnifFailure(evd,(*dummy*)NotSameHead)
 
 and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
@@ -973,14 +974,14 @@ let apply_on_subterm env evdref f c t =
   in
   applyrec (env,(0,c)) t
 
-let filter_possible_projections c ty ctxt args =
+let filter_possible_projections evd c ty ctxt args =
   (* Since args in the types will be replaced by holes, we count the
      fv of args to have a well-typed filter; don't know how necessary
      it is however to have a well-typed filter here *)
-  let fv1 = free_rels (mkApp (c,args)) (* Hack: locally untyped *) in
-  let fv2 = collect_vars (mkApp (c,args)) in
+  let fv1 = free_rels evd (EConstr.of_constr (mkApp (c,args))) (* Hack: locally untyped *) in
+  let fv2 = collect_vars evd (EConstr.of_constr (mkApp (c,args))) in
   let len = Array.length args in
-  let tyvars = collect_vars ty in
+  let tyvars = collect_vars evd (EConstr.of_constr ty) in
   List.map_i (fun i decl ->
     let () = assert (i < len) in
     let a = Array.unsafe_get args i in
@@ -1039,7 +1040,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
       let t = NamedDecl.get_type decl' in
       let evs = ref [] in
       let ty = Retyping.get_type_of env_rhs evd c in
-      let filter' = filter_possible_projections c ty ctxt args in
+      let filter' = filter_possible_projections evd c ty ctxt args in
       (id,t,c,ty,evs,Filter.make filter',occs) :: make_subst (ctxt',l,occsl)
   | _, _, [] -> []
   | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list") in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index bafb009f5..ea3ab17a7 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -73,7 +73,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
   (** Refresh the types of evars under template polymorphic references *)
   and refresh_term_evars onevars top t =
     match kind_of_term (whd_evar !evdref t) with
-    | App (f, args) when is_template_polymorphic env f ->
+    | App (f, args) when is_template_polymorphic env !evdref (EConstr.of_constr f) ->
       let pos = get_polymorphic_positions f in
 	refresh_polymorphic_positions args pos
     | App (f, args) when top && isEvar f -> 
@@ -356,14 +356,15 @@ let expansion_of_var aliases x =
   | [] -> x
   | a::_ -> a
 
-let rec expand_vars_in_term_using aliases t = match kind_of_term t with
+let rec expand_vars_in_term_using sigma aliases t = match kind_of_term t with
   | Rel _ | Var _ ->
       normalize_alias aliases t
   | _ ->
-      map_constr_with_full_binders
-        extend_alias expand_vars_in_term_using aliases t
+    let self aliases c = EConstr.of_constr (expand_vars_in_term_using sigma aliases (EConstr.Unsafe.to_constr c)) in
+    EConstr.Unsafe.to_constr (map_constr_with_full_binders sigma
+        extend_alias self aliases (EConstr.of_constr t))
 
-let expand_vars_in_term env = expand_vars_in_term_using (make_alias_map env)
+let expand_vars_in_term env sigma = expand_vars_in_term_using sigma (make_alias_map env)
 
 let free_vars_and_rels_up_alias_expansion aliases c =
   let acc1 = ref Int.Set.empty and acc2 = ref Id.Set.empty in
@@ -430,8 +431,8 @@ let constr_list_distinct l =
     | [] -> true
   in loop l
 
-let get_actual_deps aliases l t =
-  if occur_meta_or_existential t then
+let get_actual_deps evd aliases l t =
+  if occur_meta_or_existential evd (EConstr.of_constr t) then
     (* Probably no restrictions on allowed vars in presence of evars *)
     l
   else
@@ -460,21 +461,21 @@ let remove_instance_local_defs evd evk args =
 
 (* Check if an applied evar "?X[args] l" is a Miller's pattern *)
 
-let find_unification_pattern_args env l t =
+let find_unification_pattern_args env evd l t =
   if List.for_all (fun x -> isRel x || isVar x) l (* common failure case *) then
     let aliases = make_alias_map env in
     match (try Some (expand_and_check_vars aliases l) with Exit -> None) with
-    | Some l as x when constr_list_distinct (get_actual_deps aliases l t) -> x
+    | Some l as x when constr_list_distinct (get_actual_deps evd aliases l t) -> x
     | _ -> None
   else
     None
 
-let is_unification_pattern_meta env nb m l t =
+let is_unification_pattern_meta env evd nb m l t =
   (* Variables from context and rels > nb are implicitly all there *)
   (* so we need to be a rel <= nb *)
   if List.for_all (fun x -> isRel x && destRel x <= nb) l then
-    match find_unification_pattern_args env l t with
-    | Some _ as x when not (dependent (mkMeta m) t) -> x
+    match find_unification_pattern_args env evd l t with
+    | Some _ as x when not (dependent evd (EConstr.mkMeta m) (EConstr.of_constr t)) -> x
     | _ -> None
   else
     None
@@ -485,7 +486,7 @@ let is_unification_pattern_evar env evd (evk,args) l t =
   then
     let args = remove_instance_local_defs evd evk args in
     let n = List.length args in
-      match find_unification_pattern_args env (args @ l) t with
+      match find_unification_pattern_args env evd (args @ l) t with
       | Some l -> Some (List.skipn n l)
       | _ -> None
   else None
@@ -498,7 +499,7 @@ let is_unification_pattern_pure_evar env evd (evk,args) t =
 
 let is_unification_pattern (env,nb) evd f l t =
   match kind_of_term f with
-  | Meta m -> is_unification_pattern_meta env nb m l t
+  | Meta m -> is_unification_pattern_meta env evd nb m l t
   | Evar ev -> is_unification_pattern_evar env evd ev l t
   | _ -> None
 
@@ -509,9 +510,9 @@ let is_unification_pattern (env,nb) evd f l t =
    *implicitly* depend on Vars but lambda abstraction will not reflect this
    dependency: ?X x = ?1 (?1 is a meta) will return \_.?1 while it should
    return \y. ?1{x\y} (non constant function if ?1 depends on x) (BB) *)
-let solve_pattern_eqn env l c =
+let solve_pattern_eqn env sigma l c =
   let c' = List.fold_right (fun a c ->
-    let c' = subst_term (lift 1 a) (lift 1 c) in
+    let c' = subst_term sigma (EConstr.of_constr (lift 1 a)) (EConstr.of_constr (lift 1 c)) in
     match kind_of_term a with
       (* Rem: if [a] links to a let-in, do as if it were an assumption *)
       | Rel n ->
@@ -550,7 +551,7 @@ let make_projectable_subst aliases sigma evi args =
         | LocalAssum (id,c), a::rest ->
             let a = whd_evar sigma a in
             let cstrs =
-              let a',args = decompose_app_vect a in
+              let a',args = decompose_app_vect sigma (EConstr.of_constr a) in
               match kind_of_term a' with
               | Construct cstr ->
                   let l = try Constrmap.find (fst cstr) cstrs with Not_found -> [] in
@@ -923,12 +924,12 @@ let invert_invertible_arg fullenv evd aliases k (evk,argsv) args' =
 let set_of_evctx l =
   List.fold_left (fun s decl -> Id.Set.add (get_id decl) s) Id.Set.empty l
 
-let filter_effective_candidates evi filter candidates =
+let filter_effective_candidates evd evi filter candidates =
   match filter with
   | None -> candidates
   | Some filter ->
       let ids = set_of_evctx (Filter.filter_list filter (evar_context evi)) in
-      List.filter (fun a -> Id.Set.subset (collect_vars a) ids) candidates
+      List.filter (fun a -> Id.Set.subset (collect_vars evd (EConstr.of_constr a)) ids) candidates
 
 let filter_candidates evd evk filter candidates_update =
   let evi = Evd.find_undefined evd evk in
@@ -939,7 +940,7 @@ let filter_candidates evd evk filter candidates_update =
   match candidates with
   | None -> NoUpdate
   | Some l ->
-      let l' = filter_effective_candidates evi filter l in
+      let l' = filter_effective_candidates evd evi filter l in
       if List.length l = List.length l' && candidates_update = NoUpdate then
         NoUpdate
       else
@@ -952,7 +953,7 @@ let closure_of_filter evd evk = function
   | None -> None
   | Some filter ->
   let evi = Evd.find_undefined evd evk in
-  let vars = collect_vars (Evarutil.nf_evar evd (evar_concl evi)) in
+  let vars = collect_vars evd (EConstr.of_constr (evar_concl evi)) in
   let test b decl = b || Idset.mem (get_id decl) vars ||
                     match decl with
                     | LocalAssum _ ->
@@ -999,7 +1000,7 @@ let do_restrict_hyps evd (evk,args as ev) filter candidates =
 (* ?e is assumed to have no candidates *)
 
 let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs =
-  let rhs = expand_vars_in_term env rhs in
+  let rhs = expand_vars_in_term env evd rhs in
   let filter =
     restrict_upon_filter evd evk
       (* Keep only variables that occur in rhs *)
@@ -1010,7 +1011,7 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs =
       (* expands only rels and vars aliases, not rels or vars bound to an *)
       (* arbitrary complex term *)
       (fun a -> not (isRel a || isVar a)
-                || dependent a rhs || List.exists (fun (id,_) -> isVarId id a) sols)
+                || dependent evd (EConstr.of_constr a) (EConstr.of_constr rhs) || List.exists (fun (id,_) -> isVarId id a) sols)
       argsv in
   let filter = closure_of_filter evd evk filter in
   let candidates = extract_candidates sols in
@@ -1060,7 +1061,7 @@ let restrict_candidates conv_algo env evd filter1 (evk1,argsv1) (evk2,argsv2) =
   | _, None -> filter_candidates evd evk1 filter1 NoUpdate
   | None, Some _ -> raise DoesNotPreserveCandidateRestriction
   | Some l1, Some l2 ->
-      let l1 = filter_effective_candidates evi1 filter1 l1 in
+      let l1 = filter_effective_candidates evd evi1 filter1 l1 in
       let l1' = List.filter (fun c1 ->
         let c1' = instantiate_evar_array evi1 c1 argsv1 in
         let filter c2 =
@@ -1091,9 +1092,7 @@ exception CannotProject of evar_map * existential
 *)
 
 let rec is_constrainable_in top evd k (ev,(fv_rels,fv_ids) as g) t =
-  let f,args2 = decompose_app_vect t in
-  let f,args1 = decompose_app_vect (whd_evar evd f) in
-  let args = Array.append args1 args2 in
+  let f,args = decompose_app_vect evd (EConstr.of_constr t) in
   match kind_of_term f with
   | Construct ((ind,_),u) ->
     let n = Inductiveops.inductive_nparams ind in
@@ -1450,7 +1449,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
     | _ ->
         progress := true;
         match
-          let c,args = decompose_app_vect t in
+          let c,args = decompose_app_vect !evdref (EConstr.of_constr t) in
           match kind_of_term c with
           | Construct (cstr,u) when noccur_between 1 k t ->
             (* This is common case when inferring the return clause of match *)
@@ -1466,10 +1465,11 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
             let ty = get_type_of env' !evdref t in
             let candidates =
               try
+                let self env c = EConstr.of_constr (imitate env (EConstr.Unsafe.to_constr c)) in
                 let t =
-                  map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
-                    imitate envk t in
-                t::l
+                  map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1)
+                    self envk (EConstr.of_constr t) in
+                EConstr.Unsafe.to_constr t::l
               with e when CErrors.noncritical e -> l in
             (match candidates with
             | [x] -> x
@@ -1480,8 +1480,9 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
               evar'')
         | None ->
            (* Evar/Rigid problem (or assimilated if not normal): we "imitate" *)
-	   map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
-					imitate envk t
+          let self env c = EConstr.of_constr (imitate env (EConstr.Unsafe.to_constr c)) in
+          EConstr.Unsafe.to_constr (map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1)
+					self envk (EConstr.of_constr t))
   in
   let rhs = whd_beta evd rhs (* heuristic *) in
   let fast rhs = 
@@ -1498,7 +1499,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
     in
       is_id_subst filter_ctxt (Array.to_list argsv) &&
       closed0 rhs &&
-      Idset.subset (collect_vars rhs) !names 
+      Idset.subset (collect_vars evd (EConstr.of_constr rhs)) !names 
   in
   let body =
     if fast rhs then nf_evar evd rhs
@@ -1530,7 +1531,7 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
   with NoCandidates ->
   try
     let (evd',body) = invert_definition conv_algo choose env evd pbty ev rhs in
-    if occur_meta body then raise MetaOccurInBodyInternal;
+    if occur_meta evd' (EConstr.of_constr body) then raise MetaOccurInBodyInternal;
     (* invert_definition may have instantiate some evars of rhs with evk *)
     (* so we recheck acyclicity *)
     if occur_evar_upto_types evd' evk body then raise (OccurCheckIn (evd',body));
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index f94c83b6d..cf059febf 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -18,7 +18,7 @@ val is_success : unification_result -> bool
 
 (** Replace the vars and rels that are aliases to other vars and rels by 
    their representative that is most ancient in the context *)
-val expand_vars_in_term : env -> constr -> constr
+val expand_vars_in_term : env -> evar_map -> constr -> constr
 
 (** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]),
    possibly solving related unification problems, possibly leaving open
@@ -62,7 +62,7 @@ val is_unification_pattern_evar : env -> evar_map -> existential -> constr list
 val is_unification_pattern : env * int -> evar_map -> constr -> constr list ->
   constr -> constr list option
 
-val solve_pattern_eqn : env -> constr list -> constr -> constr
+val solve_pattern_eqn : env -> evar_map -> constr list -> constr -> constr
 
 val noccur_evar : env -> evar_map -> Evar.t -> constr -> bool
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8f369a811..9b572f376 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -751,7 +751,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       match evar_kind_of_term !evdref resj.uj_val with
       | App (f,args) ->
         let f = whd_evar !evdref f in
-          if is_template_polymorphic env.ExtraEnv.env f then
+          if is_template_polymorphic env.ExtraEnv.env !evdref (EConstr.of_constr f) then
 	    (* Special case for inductive type applications that must be 
 	       refreshed right away. *)
 	    let sigma = !evdref in
@@ -1009,7 +1009,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	  | VMcast ->
  	    let cj = pretype empty_tycon env evdref lvar c in
 	    let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in
-	      if not (occur_existential cty || occur_existential tval) then
+	      if not (occur_existential !evdref (EConstr.of_constr cty) || occur_existential !evdref (EConstr.of_constr tval)) then
 		let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in
 		if b then (evdref := evd; cj, tval)
 		else
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index cda052b79..e897d5f5c 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -171,7 +171,7 @@ let keep_true_projections projs kinds =
   let filter (p, (_, b)) = if b then Some p else None in
   List.map_filter filter (List.combine projs kinds)
 
-let cs_pattern_of_constr t =
+let cs_pattern_of_constr sigma t =
   match kind_of_term t with
       App (f,vargs) ->
 	begin
@@ -179,7 +179,7 @@ let cs_pattern_of_constr t =
           with e when CErrors.noncritical e -> raise Not_found
 	end
     | Rel n -> Default_cs, Some n, []
-    | Prod (_,a,b) when not (Termops.dependent (mkRel 1) b) -> Prod_cs, None, [a; Termops.pop b]
+    | Prod (_,a,b) when EConstr.Vars.noccurn sigma 1 (EConstr.of_constr b) -> Prod_cs, None, [a; Termops.pop (EConstr.of_constr b)]
     | Sort s -> Sort_cs (family_of_sort s), None, []
     | _ ->
 	begin
@@ -217,7 +217,7 @@ let compute_canonical_projections warn (con,ind) =
            | Some proji_sp ->
 	       begin
 		 try
-		   let patt, n , args = cs_pattern_of_constr t in
+		   let patt, n , args = cs_pattern_of_constr Evd.empty t (** FIXME *) in
 		     ((ConstRef proji_sp, patt, t, n, args) :: l)
 		 with Not_found ->
                      let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con)
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index a6a90c751..4a176760c 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -65,7 +65,7 @@ type obj_typ = {
   o_TCOMPS : constr list } (** ordered *)
 
 (** Return the form of the component of a canonical structure *)
-val cs_pattern_of_constr : constr -> cs_pattern * int option * constr list
+val cs_pattern_of_constr : Evd.evar_map -> constr -> cs_pattern * int option * constr list
 
 val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index a85e493ea..820974888 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -197,14 +197,14 @@ module Cst_stack = struct
 
   (** [best_replace d cst_l c] makes the best replacement for [d]
       by [cst_l] in [c] *)
-  let best_replace d cst_l c =
+  let best_replace sigma d cst_l c =
     let reconstruct_head = List.fold_left
       (fun t (i,args) -> mkApp (t,Array.sub args i (Array.length args - i))) in
     List.fold_right
-      (fun (cst,params,args) t -> Termops.replace_term
-	(reconstruct_head d args)
-	(applist (cst, List.rev params))
-	t) cst_l c
+      (fun (cst,params,args) t -> Termops.replace_term sigma
+	(EConstr.of_constr (reconstruct_head d args))
+	(EConstr.of_constr (applist (cst, List.rev params)))
+	(EConstr.of_constr t)) cst_l c
 
   let pr l =
     let open Pp in
@@ -612,8 +612,9 @@ let safe_meta_value sigma ev =
 
 let strong whdfun env sigma t =
   let rec strongrec env t =
-    map_constr_with_full_binders push_rel strongrec env (whdfun env sigma t) in
-  strongrec env t
+    let t = EConstr.of_constr (whdfun env sigma (EConstr.Unsafe.to_constr t)) in
+    map_constr_with_full_binders sigma push_rel strongrec env t in
+  EConstr.Unsafe.to_constr (strongrec env (EConstr.of_constr t))
 
 let local_strong whdfun sigma =
   let rec strongrec t = Constr.map strongrec (whdfun sigma t) in
@@ -712,14 +713,14 @@ let contract_cofix ?env ?reference (bodynum,(names,types,bodies as typedbodies))
   substl closure bodies.(bodynum)
 
 (** Similar to the "fix" case below *)
-let reduce_and_refold_cofix recfun env refold cst_l cofix sk =
+let reduce_and_refold_cofix recfun env sigma refold cst_l cofix sk =
   let raw_answer =
     let env = if refold then Some env else None in
     contract_cofix ?env ?reference:(Cst_stack.reference cst_l) cofix in
   apply_subst
     (fun x (t,sk') ->
       let t' =
-        if refold then Cst_stack.best_replace (mkCoFix cofix) cst_l t else t in
+        if refold then Cst_stack.best_replace sigma (mkCoFix cofix) cst_l t else t in
       recfun x (t',sk'))
     [] refold Cst_stack.empty raw_answer sk
 
@@ -757,7 +758,7 @@ let contract_fix ?env ?reference ((recindices,bodynum),(names,types,bodies as ty
     replace the fixpoint by the best constant from [cst_l]
     Other rels are directly substituted by constants "magically found from the
     context" in contract_fix *)
-let reduce_and_refold_fix recfun env refold cst_l fix sk =
+let reduce_and_refold_fix recfun env sigma refold cst_l fix sk =
   let raw_answer =
     let env = if refold then None else Some env in
     contract_fix ?env ?reference:(Cst_stack.reference cst_l) fix in
@@ -765,7 +766,7 @@ let reduce_and_refold_fix recfun env refold cst_l fix sk =
     (fun x (t,sk') ->
       let t' =
         if refold then
-          Cst_stack.best_replace (mkFix fix) cst_l t
+          Cst_stack.best_replace sigma (mkFix fix) cst_l t
         else t
       in recfun x (t',sk'))
     [] refold Cst_stack.empty raw_answer sk
@@ -947,7 +948,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
             | Rel 1, [] ->
 	      let lc = Array.sub cl 0 (napp-1) in
 	      let u = if Int.equal napp 1 then f else appvect (f,lc) in
-	      if noccurn 1 u then (pop u,Stack.empty),Cst_stack.empty else fold ()
+	      if noccurn 1 u then (pop (EConstr.of_constr u),Stack.empty),Cst_stack.empty else fold ()
             | _ -> fold ()
 	  else fold ()
 	| _ -> fold ())
@@ -974,7 +975,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
 	|args, (Stack.Fix (f,s',cst_l)::s'') when use_fix ->
 	  let x' = Stack.zip(x,args) in
 	  let out_sk = s' @ (Stack.append_app [|x'|] s'') in
-	  reduce_and_refold_fix whrec env refold cst_l f out_sk
+	  reduce_and_refold_fix whrec env sigma refold cst_l f out_sk
 	|args, (Stack.Cst (const,curr,remains,s',cst_l) :: s'') ->
 	  let x' = Stack.zip(x,args) in
 	  begin match remains with
@@ -1010,7 +1011,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
       if CClosure.RedFlags.red_set flags CClosure.RedFlags.fCOFIX then
 	match Stack.strip_app stack with
 	|args, ((Stack.Case _ |Stack.Proj _)::s') ->
-	  reduce_and_refold_cofix whrec env refold cst_l cofix stack
+	  reduce_and_refold_cofix whrec env sigma refold cst_l cofix stack
 	|_ -> fold ()
       else fold ()
 
@@ -1043,7 +1044,7 @@ let local_whd_state_gen flags sigma =
             | Rel 1, [] ->
 	      let lc = Array.sub cl 0 (napp-1) in
 	      let u = if Int.equal napp 1 then f else appvect (f,lc) in
-	      if noccurn 1 u then (pop u,Stack.empty) else s
+	      if noccurn 1 u then (pop (EConstr.of_constr u),Stack.empty) else s
             | _ -> s
 	  else s
 	| _ -> s)
@@ -1568,10 +1569,10 @@ let meta_reducible_instance evd b =
   in
   let metas = Metaset.fold fold fm Metamap.empty in
   let rec irec u =
-    let u = whd_betaiota Evd.empty u in
+    let u = whd_betaiota Evd.empty u (** FIXME *) in
     match kind_of_term u with
-    | Case (ci,p,c,bl) when isMeta (strip_outer_cast c) ->
-	let m = destMeta (strip_outer_cast c) in
+    | Case (ci,p,c,bl) when EConstr.isMeta evd (EConstr.of_constr (strip_outer_cast evd (EConstr.of_constr c))) ->
+	let m = destMeta (strip_outer_cast evd (EConstr.of_constr c)) in
 	(match
 	  try
 	    let g, s = Metamap.find m metas in
@@ -1581,8 +1582,8 @@ let meta_reducible_instance evd b =
 	  with
 	    | Some g -> irec (mkCase (ci,p,g,bl))
 	    | None -> mkCase (ci,irec p,c,Array.map irec bl))
-    | App (f,l) when isMeta (strip_outer_cast f) ->
-	let m = destMeta (strip_outer_cast f) in
+    | App (f,l) when EConstr.isMeta evd (EConstr.of_constr (strip_outer_cast evd (EConstr.of_constr f))) ->
+	let m = destMeta (strip_outer_cast evd (EConstr.of_constr f)) in
 	(match
 	  try
 	    let g, s = Metamap.find m metas in
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 4cd7a2a86..8dcf5c084 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -44,7 +44,7 @@ module Cst_stack : sig
   val add_args : constr array -> t -> t
   val add_cst : constr -> t -> t
   val best_cst : t -> (constr * constr list) option
-  val best_replace : constr -> t -> constr -> constr
+  val best_replace : Evd.evar_map -> constr -> t -> constr -> constr
   val reference : t -> Constant.t option
   val pr : t -> Pp.std_ppcmds
 end
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 5b67af3e7..ac3b5ef63 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -93,7 +93,7 @@ let retype ?(polyprop=true) sigma =
   let rec type_of env cstr =
     match kind_of_term cstr with
     | Meta n ->
-      (try strip_outer_cast (Evd.meta_ftype sigma n).Evd.rebus
+      (try strip_outer_cast sigma (EConstr.of_constr (Evd.meta_ftype sigma n).Evd.rebus)
        with Not_found -> retype_error (BadMeta n))
     | Rel n ->
 	let ty = RelDecl.get_type (lookup_rel n env) in
@@ -124,12 +124,13 @@ let retype ?(polyprop=true) sigma =
          subst1 b (type_of (push_rel (LocalDef (name,b,c1)) env) c2)
     | Fix ((_,i),(_,tys,_)) -> tys.(i)
     | CoFix (i,(_,tys,_)) -> tys.(i)
-    | App(f,args) when is_template_polymorphic env f ->
+    | App(f,args) when is_template_polymorphic env sigma (EConstr.of_constr f) ->
+        let f = whd_evar sigma f in
 	let t = type_of_global_reference_knowing_parameters env f args in
-        strip_outer_cast (subst_type env sigma t (Array.to_list args))
+        strip_outer_cast sigma (EConstr.of_constr (subst_type env sigma t (Array.to_list args)))
     | App(f,args) ->
-        strip_outer_cast
-          (subst_type env sigma (type_of env f) (Array.to_list args))
+        strip_outer_cast sigma
+          (EConstr.of_constr (subst_type env sigma (type_of env f) (Array.to_list args)))
     | Proj (p,c) ->
        let ty = type_of env c in
        (try
@@ -152,7 +153,8 @@ let retype ?(polyprop=true) sigma =
 	  | Prop Pos, (Type u2) -> Type (Univ.sup Univ.type0_univ u2)
 	  | Prop Null, (Type _ as s) -> s
 	  | Type u1, Type u2 -> Type (Univ.sup u1 u2))
-    | App(f,args) when is_template_polymorphic env f ->
+    | App(f,args) when is_template_polymorphic env sigma (EConstr.of_constr f) ->
+      let f = whd_evar sigma f in
       let t = type_of_global_reference_knowing_parameters env f args in
         sort_of_atomic_type env sigma t args
     | App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
@@ -168,7 +170,8 @@ let retype ?(polyprop=true) sigma =
 	let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in
 	if not (is_impredicative_set env) &&
 	   s2 == InSet && sort_family_of env t == InType then InType else s2
-    | App(f,args) when is_template_polymorphic env f ->
+    | App(f,args) when is_template_polymorphic env sigma (EConstr.of_constr f) ->
+        let f = whd_evar sigma f in
 	let t = type_of_global_reference_knowing_parameters env f args in
         family_of_sort (sort_of_atomic_type env sigma t args)
     | App(f,args) ->
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 7da738508..ff76abe37 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -177,7 +177,7 @@ let eval_table = Summary.ref (Cmap.empty : frozen) ~name:"evaluation"
    the xp..x1.
 *)
 
-let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
+let check_fix_reversibility sigma labs args ((lv,i),(_,tys,bds)) =
   let n = List.length labs in
   let nargs = List.length args in
   if nargs > n then raise Elimconst;
@@ -202,7 +202,7 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
     raise Elimconst;
   List.iteri (fun i t_i ->
     if not (Int.List.mem_assoc (i+1) li) then
-      let fvs = List.map ((+) (i+1)) (Int.Set.elements (free_rels t_i)) in
+      let fvs = List.map ((+) (i+1)) (Int.Set.elements (free_rels sigma (EConstr.of_constr t_i))) in
       match List.intersect Int.equal fvs reversible_rels with
       | [] -> ()
       | _ -> raise Elimconst)
@@ -261,7 +261,7 @@ let compute_consteval_direct env sigma ref =
           let open Context.Rel.Declaration in
 	  srec (push_rel (LocalAssum (id,t)) env) (n+1) (t::labs) onlyproj g
       | Fix fix when not onlyproj ->
-	  (try check_fix_reversibility labs l fix
+	  (try check_fix_reversibility sigma labs l fix
 	  with Elimconst -> NotAnElimination)
       | Case (_,_,d,_) when isRel d && not onlyproj -> EliminationCases n
       | Case (_,_,d,_) -> srec env n labs true d
@@ -1102,13 +1102,13 @@ let fold_one_com com env sigma c =
   (* 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 (clos_norm_flags unfold_side_red env sigma rcom) c in
+  let a = subst_term sigma (EConstr.of_constr (clos_norm_flags unfold_side_red env sigma rcom)) (EConstr.of_constr c) in
   if not (eq_constr a c) then
     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 rcom c in
+    let a = subst_term sigma (EConstr.of_constr rcom) (EConstr.of_constr c) in
     subst1 com a
 
 let fold_commands cl env sigma c =
@@ -1133,8 +1133,8 @@ let compute = cbv_betadeltaiota
 let abstract_scheme env (locc,a) (c, sigma) =
   let ta = Retyping.get_type_of env sigma a in
   let na = named_hd env ta Anonymous in
-  if occur_meta ta then error "Cannot find a type for the generalisation.";
-  if occur_meta a then
+  if occur_meta sigma (EConstr.of_constr ta) then error "Cannot find a type for the generalisation.";
+  if occur_meta sigma (EConstr.of_constr a) then
     mkLambda (na,ta,c), sigma
   else
     let c', sigma' = subst_closed_term_occ env sigma (AtOccs locc) a c in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e2b3af7e9..3134dac6a 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -87,7 +87,7 @@ let abstract_scheme env evd c l lname_typ =
    are unclear...
        if occur_meta ta then error "cannot find a type for the generalisation"
        else *) 
-       if occur_meta a then mkLambda_name env (na,ta,t), evd
+       if occur_meta evd (EConstr.of_constr a) then mkLambda_name env (na,ta,t), evd
        else
 	 let t', evd' = Find_subterm.subst_closed_term_occ env evd locc a t in
 	   mkLambda_name env (na,ta,t'), evd')
@@ -182,7 +182,7 @@ let solve_pattern_eqn_array (env,nb) f l c (sigma,metasubst,evarsubst) =
 	   extra assumptions added by unification to the context *)
         let env' = pop_rel_context nb env in
 	let sigma,c = pose_all_metas_as_evars env' sigma c in
-	let c = solve_pattern_eqn env l c in
+	let c = solve_pattern_eqn env sigma l c in
 	let pb = (Conv,TypeNotProcessed) in
 	  if noccur_between 1 nb c then
             sigma,(k,lift (-nb) c,pb)::metasubst,evarsubst
@@ -190,7 +190,7 @@ let solve_pattern_eqn_array (env,nb) f l c (sigma,metasubst,evarsubst) =
     | Evar ev ->
         let env' = pop_rel_context nb env in
 	let sigma,c = pose_all_metas_as_evars env' sigma c in
-	sigma,metasubst,(env,ev,solve_pattern_eqn env l c)::evarsubst
+	sigma,metasubst,(env,ev,solve_pattern_eqn env sigma l c)::evarsubst
     | _ -> assert false
 
 let push d (env,n) = (push_rel_assum d env,n+1)
@@ -679,7 +679,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	    if k2 < k1 then sigma,(k1,cN,stN)::metasubst,evarsubst
 	    else sigma,(k2,cM,stM)::metasubst,evarsubst
 	| Meta k, _
-            when not (dependent cM cN) (* helps early trying alternatives *) ->
+            when not (dependent sigma (EConstr.of_constr cM) (EConstr.of_constr cN)) (* helps early trying alternatives *) ->
             let sigma = 
 	      if opt.with_types && flags.check_applied_meta_types then
 		(try
@@ -699,7 +699,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
               evarsubst)
 	    else error_cannot_unify_local curenv sigma (m,n,cN)
 	| _, Meta k
-            when not (dependent cN cM) (* helps early trying alternatives *) ->
+            when not (dependent sigma (EConstr.of_constr cN) (EConstr.of_constr cM)) (* helps early trying alternatives *) ->
           let sigma = 
 	    if opt.with_types && flags.check_applied_meta_types then
               (try
@@ -728,15 +728,15 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	      sigma,metasubst,((curenv,ev,cN)::evarsubst)
 	| Evar (evk,_ as ev), _
             when not (Evar.Set.mem evk flags.frozen_evars) 
-	      && not (occur_evar evk cN) ->
-	    let cmvars = free_rels cM and cnvars = free_rels cN in
+	      && not (occur_evar sigma evk (EConstr.of_constr cN)) ->
+	    let cmvars = free_rels sigma (EConstr.of_constr cM) and cnvars = free_rels sigma (EConstr.of_constr cN) in
 	      if Int.Set.subset cnvars cmvars then
 		sigma,metasubst,((curenv,ev,cN)::evarsubst)
 	      else error_cannot_unify_local curenv sigma (m,n,cN)
 	| _, Evar (evk,_ as ev)
             when not (Evar.Set.mem evk flags.frozen_evars)
-	      && not (occur_evar evk cM) ->
-	    let cmvars = free_rels cM and cnvars = free_rels cN in
+	      && not (occur_evar sigma evk (EConstr.of_constr cM)) ->
+	    let cmvars = free_rels sigma (EConstr.of_constr cM) and cnvars = free_rels sigma (EConstr.of_constr cN) in
 	      if Int.Set.subset cmvars cnvars then
 		sigma,metasubst,((curenv,ev,cM)::evarsubst)
 	      else error_cannot_unify_local curenv sigma (m,n,cN)
@@ -1295,8 +1295,8 @@ let w_merge env with_types flags (evd,metas,evars) =
 	  (* This can make rhs' ill-typed if metas are *)
           let rhs' = subst_meta_instances metas rhs in
           match kind_of_term rhs with
-	  | App (f,cl) when occur_meta rhs' ->
-	      if occur_evar evk rhs' then
+	  | App (f,cl) when occur_meta evd (EConstr.of_constr rhs') ->
+	      if occur_evar evd evk (EConstr.of_constr rhs') then
                 error_occur_check curenv evd evk rhs';
 	      if is_mimick_head flags.modulo_delta f then
 		let evd' =
@@ -1474,16 +1474,16 @@ let iter_fail f a =
 (* make_abstraction: a variant of w_unify_to_subterm which works on
    contexts, with evars, and possibly with occurrences *)
 
-let indirectly_dependent c d decls =
+let indirectly_dependent sigma c d decls =
   not (isVar c) &&
     (* This test is not needed if the original term is a variable, but
        it is needed otherwise, as e.g. when abstracting over "2" in
        "forall H:0=2, H=H:>(0=1+1) -> 0=2." where there is now obvious
        way to see that the second hypothesis depends indirectly over 2 *)
-    List.exists (fun d' -> dependent_in_decl (mkVar (NamedDecl.get_id d')) d) decls
+    List.exists (fun d' -> dependent_in_decl sigma (EConstr.mkVar (NamedDecl.get_id d')) d) decls
 
-let indirect_dependency d decls =
-  decls  |>  List.filter (fun d' -> dependent_in_decl (mkVar (NamedDecl.get_id d')) d)  |>  List.hd  |>  NamedDecl.get_id
+let indirect_dependency sigma d decls =
+  decls  |>  List.filter (fun d' -> dependent_in_decl sigma (EConstr.mkVar (NamedDecl.get_id d')) d)  |>  List.hd  |>  NamedDecl.get_id
 
 let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) =
   let current_sigma = Sigma.to_evar_map current_sigma in
@@ -1610,7 +1610,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
         let occ = if likefirst then LikeFirst else AtOccs occ in
         let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in
         if Context.Named.Declaration.equal d newdecl
-           && not (indirectly_dependent c d depdecls)
+           && not (indirectly_dependent sigma c d depdecls)
         then
           if check_occs && not (in_every_hyp occs)
           then raise (PretypeError (env,sigma,NoOccurrenceFound (c,Some hyp)))
@@ -1695,13 +1695,13 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
   let bestexn = ref None in
   let kop = Keys.constr_key op in
   let rec matchrec cl =
-    let cl = strip_outer_cast cl in
+    let cl = strip_outer_cast evd (EConstr.of_constr cl) in
     (try
        if closed0 cl && not (isEvar cl) && keyed_unify env evd kop cl then
        (try
          if !keyed_unification then
-           let f1, l1 = decompose_app_vect op in
-	   let f2, l2 = decompose_app_vect cl in
+           let f1, l1 = decompose_app_vect evd (EConstr.of_constr op) in
+	   let f2, l2 = decompose_app_vect evd (EConstr.of_constr cl) in
 	   w_typed_unify_array env evd flags f1 l1 f2 l2,cl
 	 else w_typed_unify env evd CONV flags op cl,cl
        with ex when Pretype_errors.unsatisfiable_exception ex ->
@@ -1788,7 +1788,7 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) =
     in ffail 0
   in
   let rec matchrec cl =
-    let cl = strip_outer_cast cl in
+    let cl = strip_outer_cast evd (EConstr.of_constr cl) in
       (bind
 	  (if closed0 cl
 	  then return (fun () -> w_typed_unify env evd CONV flags op cl,cl)
@@ -1839,7 +1839,7 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t =
       else
         let allow_K = flags.allow_K_in_toplevel_higher_order_unification in
         let flags =
-          if occur_meta_or_existential op || !keyed_unification then
+          if occur_meta_or_existential evd (EConstr.of_constr op) || !keyed_unification then
 	    (* This is up to delta for subterms w/o metas ... *)
             flags
           else
@@ -1848,7 +1848,7 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t =
                unify pre-existing non frozen evars of the goal or of the
                pattern *)
           set_no_delta_flags flags in
-	let t' = (strip_outer_cast op,t) in
+	let t' = (strip_outer_cast evd (EConstr.of_constr op),t) in
         let (evd',cl) =
           try
   	    if is_keyed_unification () then
@@ -1864,7 +1864,7 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t =
                 (* w_unify_to_subterm does not go through evars, so
                    the next step, which was already in <= 8.4, is
                    needed at least for compatibility of rewrite *)
-                dependent op t -> (evd,op)
+                dependent evd (EConstr.of_constr op) (EConstr.of_constr t) -> (evd,op)
         in
 	  if not allow_K &&
             (* ensure we found a different instance *)