Termops API using EConstr.

15 files changed, 223 insertions, 198 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index d4251555d8..17fe7362d2 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -302,7 +302,7 @@ let hintmap_of secvars hdc concl =
   match hdc with
   | None -> Hint_db.map_none ~secvars
   | Some hdc ->
-     if occur_existential concl then
+     if occur_existential Evd.empty (EConstr.of_constr concl) then (** FIXME *)
        Hint_db.map_existential ~secvars hdc concl
      else Hint_db.map_auto ~secvars hdc concl
 
@@ -329,11 +329,12 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
   in
   Proofview.Goal.enter { enter = begin fun gl ->
     let concl = Tacmach.New.pf_nf_concl gl in
+    let sigma = Tacmach.New.project gl in
     let secvars = compute_secvars gl in
     Tacticals.New.tclFIRST
       ((dbg_assumption dbg)::intro_tac::
           (List.map Tacticals.New.tclCOMPLETE
-             (trivial_resolve dbg mod_delta db_list local_db secvars concl)))
+             (trivial_resolve sigma dbg mod_delta db_list local_db secvars concl)))
   end }
 
 and my_find_search_nodelta db_list local_db secvars hdc concl =
@@ -346,7 +347,7 @@ and my_find_search mod_delta =
 
 and my_find_search_delta db_list local_db secvars hdc concl =
   let f = hintmap_of secvars hdc concl in
-    if occur_existential concl then
+    if occur_existential Evd.empty (EConstr.of_constr concl) (** FIXME *) then
       List.map_append
 	(fun db ->
 	  if Hint_db.use_dn db then
@@ -402,10 +403,10 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=
   in
   tclLOG dbg pr_hint (run_hint t tactic)
 
-and trivial_resolve dbg mod_delta db_list local_db secvars cl =
+and trivial_resolve sigma dbg mod_delta db_list local_db secvars cl =
   try
     let head =
-      try let hdconstr = decompose_app_bound cl in
+      try let hdconstr = decompose_app_bound sigma cl in
 	    Some hdconstr
       with Bound -> None
     in
@@ -449,10 +450,10 @@ let h_trivial ?(debug=Off) lems l = gen_trivial ~debug lems l
 (*                       The classical Auto tactic                        *)
 (**************************************************************************)
 
-let possible_resolve dbg mod_delta db_list local_db secvars cl =
+let possible_resolve sigma dbg mod_delta db_list local_db secvars cl =
   try
     let head =
-      try let hdconstr = decompose_app_bound cl in
+      try let hdconstr = decompose_app_bound sigma cl in
 	    Some hdconstr
       with Bound -> None
     in
@@ -488,12 +489,13 @@ let search d n mod_delta db_list local_db =
 	  (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
 	     ( Proofview.Goal.enter { enter = begin fun gl ->
                let concl = Tacmach.New.pf_nf_concl gl in
+               let sigma = Tacmach.New.project gl in
                let secvars = compute_secvars gl in
 	       let d' = incr_dbg d in
 	       Tacticals.New.tclFIRST
 	         (List.map
 		    (fun ntac -> Tacticals.New.tclTHEN ntac (search d' (n-1) local_db))
-		    (possible_resolve d mod_delta db_list local_db secvars concl))
+		    (possible_resolve sigma d mod_delta db_list local_db secvars concl))
              end }))
     end []
   in
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index a4243164ed..fe7a09f77d 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -279,9 +279,9 @@ let clenv_of_prods poly nprods (c, clenv) gl =
   let (c, _, _) = c in
   if poly || Int.equal nprods 0 then Some (None, clenv)
   else
-    let ty = Retyping.get_type_of (Proofview.Goal.env gl)
-                                  (Sigma.to_evar_map (Proofview.Goal.sigma gl)) c in
-    let diff = nb_prod ty - nprods in
+    let sigma = Tacmach.New.project gl in
+    let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma c in
+    let diff = nb_prod sigma (EConstr.of_constr ty) - nprods in
     if Pervasives.(>=) diff 0 then
       (* Was Some clenv... *)
       Some (Some diff,
@@ -454,13 +454,13 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
 and e_trivial_resolve db_list local_db secvars only_classes sigma concl =
   try
     e_my_find_search db_list local_db secvars
-     (decompose_app_bound concl) true only_classes sigma concl
+     (decompose_app_bound sigma concl) true only_classes sigma concl
   with Bound | Not_found -> []
 
 let e_possible_resolve db_list local_db secvars only_classes sigma concl =
   try
     e_my_find_search db_list local_db secvars
-      (decompose_app_bound concl) false only_classes sigma concl
+      (decompose_app_bound sigma concl) false only_classes sigma concl
   with Bound | Not_found -> []
 
 let cut_of_hints h =
@@ -666,7 +666,7 @@ module V85 = struct
 
   let needs_backtrack env evd oev concl =
     if Option.is_empty oev || is_Prop env evd concl then
-      occur_existential concl
+      occur_existential evd (EConstr.of_constr concl)
     else true
 
   let hints_tac hints sk fk {it = gl,info; sigma = s} =
@@ -740,7 +740,7 @@ module V85 = struct
              let fk' =
                (fun e ->
                  let do_backtrack =
-                   if unique then occur_existential concl
+                   if unique then occur_existential s' (EConstr.of_constr concl)
                    else if info.unique then true
                    else if List.is_empty gls' then
                      needs_backtrack env s' info.is_evar concl
@@ -975,7 +975,7 @@ module Search = struct
       NOT backtrack. *)
   let needs_backtrack env evd unique concl =
     if unique || is_Prop env evd concl then
-      occur_existential concl
+      occur_existential evd (EConstr.of_constr concl)
     else true
 
   let mark_unresolvables sigma goals =
@@ -1486,16 +1486,17 @@ let _ =
 (** Take the head of the arity of a constr.
     Used in the partial application tactic. *)
 
-let rec head_of_constr t =
-  let t = strip_outer_cast(collapse_appl t) in
+let rec head_of_constr sigma t =
+  let t = strip_outer_cast sigma (EConstr.of_constr (collapse_appl sigma (EConstr.of_constr t))) in
     match kind_of_term t with
-    | Prod (_,_,c2)  -> head_of_constr c2
-    | LetIn (_,_,_,c2) -> head_of_constr c2
-    | App (f,args)  -> head_of_constr f
+    | Prod (_,_,c2)  -> head_of_constr sigma c2
+    | LetIn (_,_,_,c2) -> head_of_constr sigma c2
+    | App (f,args)  -> head_of_constr sigma f
     | _      -> t
 
 let head_of_constr h c =
-  let c = head_of_constr c in
+  Proofview.tclEVARMAP >>= fun sigma ->
+  let c = head_of_constr sigma c in
   letin_tac None (Name h) c None Locusops.allHyps
 
 let not_evar c =
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 6b29f574cc..fcbad4bf0d 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -66,12 +66,12 @@ let contradiction_context =
           let id = NamedDecl.get_id d in
           let typ = nf_evar sigma (NamedDecl.get_type d) in
 	  let typ = whd_all env sigma typ in
-	  if is_empty_type typ then
+	  if is_empty_type sigma typ then
 	    simplest_elim (mkVar id)
 	  else match kind_of_term typ with
-	  | Prod (na,t,u) when is_empty_type u ->
+	  | Prod (na,t,u) when is_empty_type sigma u ->
              let is_unit_or_eq =
-               if use_negated_unit_or_eq_type () then match_with_unit_or_eq_type t
+               if use_negated_unit_or_eq_type () then match_with_unit_or_eq_type sigma t
                else None in
 	     Tacticals.New.tclORELSE
                (match is_unit_or_eq with
@@ -105,7 +105,7 @@ let is_negation_of env sigma typ t =
   match kind_of_term (whd_all env sigma t) with
     | Prod (na,t,u) ->
       let u = nf_evar sigma u in
-      is_empty_type u && is_conv_leq env sigma typ t
+      is_empty_type sigma u && is_conv_leq env sigma typ t
     | _ -> false
 
 let contradiction_term (c,lbind as cl) =
@@ -115,7 +115,7 @@ let contradiction_term (c,lbind as cl) =
     let type_of = Tacmach.New.pf_unsafe_type_of gl in
     let typ = type_of c in
     let _, ccl = splay_prod env sigma typ in
-    if is_empty_type ccl then
+    if is_empty_type sigma ccl then
       Tacticals.New.tclTHEN
         (elim false None cl None)
         (Tacticals.New.tclTRY assumption)
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 10c975b8d8..6250fef2d6 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -32,7 +32,8 @@ let e_give_exact ?(flags=eauto_unif_flags) c =
   Proofview.Goal.enter { enter = begin fun gl ->
   let t1 = Tacmach.New.pf_unsafe_type_of gl c in
   let t2 = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in
-  if occur_existential t1 || occur_existential t2 then
+  let sigma = Tacmach.New.project gl in
+  if occur_existential sigma (EConstr.of_constr t1) || occur_existential sigma (EConstr.of_constr t2) then
      Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c)
   else exact_check c
   end }
@@ -123,7 +124,7 @@ let hintmap_of secvars hdc concl =
   match hdc with
   | None -> fun db -> Hint_db.map_none ~secvars db
   | Some hdc ->
-     if occur_existential concl then
+     if occur_existential Evd.empty (EConstr.of_constr concl) then (** FIXME *)
        (fun db -> Hint_db.map_existential ~secvars hdc concl db)
      else (fun db -> Hint_db.map_auto ~secvars hdc concl db)
    (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)
@@ -147,7 +148,7 @@ let rec e_trivial_fail_db db_list local_db =
   let tacl =
     registered_e_assumption ::
     (Tacticals.New.tclTHEN Tactics.intro next) ::
-    (List.map fst (e_trivial_resolve db_list local_db secvars (Tacmach.New.pf_nf_concl gl)))
+    (List.map fst (e_trivial_resolve (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_nf_concl gl)))
   in
   Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl)
   end }
@@ -181,13 +182,13 @@ and e_my_find_search db_list local_db secvars hdc concl =
   in
   List.map tac_of_hint hintl
 
-and e_trivial_resolve db_list local_db secvars gl =
-  let hd = try Some (decompose_app_bound gl) with Bound -> None in
+and e_trivial_resolve sigma db_list local_db secvars gl =
+  let hd = try Some (decompose_app_bound sigma gl) with Bound -> None in
   try priority (e_my_find_search db_list local_db secvars hd gl)
   with Not_found -> []
 
-let e_possible_resolve db_list local_db secvars gl =
-  let hd = try Some (decompose_app_bound gl) with Bound -> None in
+let e_possible_resolve sigma db_list local_db secvars gl =
+  let hd = try Some (decompose_app_bound sigma gl) with Bound -> None in
   try List.map (fun (b, (tac, pp)) -> (tac, b, pp))
                (e_my_find_search db_list local_db secvars hd gl)
   with Not_found -> []
@@ -289,7 +290,7 @@ module SearchProblem = struct
 	let l =
           let concl = Reductionops.nf_evar (project g)(pf_concl g) in
 	  filter_tactics s.tacres
-                         (e_possible_resolve s.dblist (List.hd s.localdb) secvars concl)
+                         (e_possible_resolve (project g) s.dblist (List.hd s.localdb) secvars concl)
 	in
 	List.map
 	  (fun (lgls, cost, pp) ->
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 3f0c01a29c..12d8e98c43 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -79,11 +79,12 @@ let up_to_delta = ref false (* true *)
 let general_decompose recognizer c =
   Proofview.Goal.enter { enter = begin fun gl ->
   let type_of = pf_unsafe_type_of gl in
+  let sigma = project gl in
   let typc = type_of c in
   tclTHENS (cut typc)
     [ tclTHEN (intro_using tmphyp_name)
          (onLastHypId
-	    (ifOnHyp recognizer (general_decompose_aux recognizer)
+	    (ifOnHyp (recognizer sigma) (general_decompose_aux (recognizer sigma))
 	      (fun id -> clear [id])));
        exact_no_check c ]
   end }
@@ -102,17 +103,17 @@ let head_in indl t gl =
 let decompose_these c l =
   Proofview.Goal.enter { enter = begin fun gl ->
   let indl = List.map (fun x -> x, Univ.Instance.empty) l in
-  general_decompose (fun (_,t) -> head_in indl t gl) c
+  general_decompose (fun sigma (_,t) -> head_in indl t gl) c
   end }
 
 let decompose_and c =
   general_decompose
-    (fun (_,t) -> is_record t)
+    (fun sigma (_,t) -> is_record sigma t)
     c
 
 let decompose_or c =
   general_decompose
-    (fun (_,t) -> is_disjunction t)
+    (fun sigma (_,t) -> is_disjunction sigma t)
     c
 
 let h_decompose l c = decompose_these c l
@@ -133,7 +134,7 @@ let induction_trailer abs_i abs_j bargs =
        (fun id ->
           Proofview.Goal.nf_enter { enter = begin fun gl ->
 	  let idty = pf_unsafe_type_of gl (mkVar id) in
-	  let fvty = global_vars (pf_env gl) idty in
+	  let fvty = global_vars (pf_env gl) (project gl) (EConstr.of_constr idty) in
 	  let possible_bring_hyps =
 	    (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums
           in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7c819edadc..74f6dd44ae 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -405,7 +405,7 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars d
   let isatomic = isProd (whd_zeta evd hdcncl) in
   let dep_fun = if isatomic then dependent else dependent_no_evar in
   let type_of_cls = type_of_clause cls gl in
-  let dep = dep_proof_ok && dep_fun c type_of_cls in
+  let dep = dep_proof_ok && dep_fun evd (EConstr.of_constr c) (EConstr.of_constr type_of_cls) in
   let Sigma ((elim, effs), sigma, p) = find_elim hdcncl lft2rgt dep cls (Some t) gl in
   let tac =
       Proofview.tclEFFECTS effs <*>
@@ -442,7 +442,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
       let env = Proofview.Goal.env gl in
     let ctype = get_type_of env sigma c in
     let rels, t = decompose_prod_assum (whd_betaiotazeta sigma ctype) in
-      match match_with_equality_type t with
+      match match_with_equality_type sigma t with
       | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *)
 	  let lft2rgt = adjust_rewriting_direction args lft2rgt in
           leibniz_rewrite_ebindings_clause cls lft2rgt tac c (it_mkProd_or_LetIn t rels)
@@ -455,9 +455,10 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
             end
             begin function
               | (e, info) ->
+                  Proofview.tclEVARMAP >>= fun sigma ->
 	          let env' = push_rel_context rels env in
 	          let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *)
-	          match match_with_equality_type t' with
+	          match match_with_equality_type sigma t' with
 	            | Some (hdcncl,args) ->
 		  let lft2rgt = adjust_rewriting_direction args lft2rgt in
 		  leibniz_rewrite_ebindings_clause cls lft2rgt tac c
@@ -932,9 +933,10 @@ let rec build_discriminator env sigma dirn c = function
 
 let gen_absurdity id =
   Proofview.Goal.enter { enter = begin fun gl ->
+  let sigma = project gl in
   let hyp_typ = pf_get_hyp_typ id (Proofview.Goal.assume gl) in
   let hyp_typ = pf_nf_evar gl hyp_typ in
-  if is_empty_type hyp_typ
+  if is_empty_type sigma hyp_typ
   then
     simplest_elim (mkVar id)
   else
@@ -973,7 +975,7 @@ let apply_on_clause (f,t) clause =
   let sigma =  clause.evd in
   let f_clause = mk_clenv_from_env clause.env sigma None (f,t) in
   let argmv =
-    (match kind_of_term (last_arg f_clause.templval.Evd.rebus) with
+    (match kind_of_term (last_arg f_clause.evd (EConstr.of_constr f_clause.templval.Evd.rebus)) with
      | Meta mv -> mv
      | _  -> user_err  (str "Ill-formed clause applicator.")) in
   clenv_fchain ~with_univs:false argmv f_clause clause
@@ -1025,7 +1027,7 @@ let onNegatedEquality with_evars tac =
     let ccl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
     match kind_of_term (hnf_constr env sigma ccl) with
-    | Prod (_,t,u) when is_empty_type u ->
+    | Prod (_,t,u) when is_empty_type sigma u ->
         tclTHEN introf
           (onLastHypId (fun id ->
             onEquality with_evars tac (mkVar id,NoBindings)))
@@ -1079,7 +1081,7 @@ let find_sigma_data env s = build_sigma_type ()
  *)
 
 let make_tuple env sigma (rterm,rty) lind =
-  assert (dependent (mkRel lind) rty);
+  assert (not (EConstr.Vars.noccurn sigma lind (EConstr.of_constr rty)));
   let sigdata = find_sigma_data env (get_sort_of env sigma rty) in
   let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in
   let na = Context.Rel.Declaration.get_name (lookup_rel lind env) in
@@ -1101,9 +1103,9 @@ let make_tuple env sigma (rterm,rty) lind =
    normalization *)
 
 let minimal_free_rels env sigma (c,cty) =
-  let cty_rels = free_rels cty in
+  let cty_rels = free_rels sigma (EConstr.of_constr cty) in
   let cty' = simpl env sigma cty in
-  let rels' = free_rels cty' in
+  let rels' = free_rels sigma (EConstr.of_constr cty') in
   if Int.Set.subset cty_rels rels' then
     (cty,cty_rels)
   else
@@ -1302,6 +1304,7 @@ let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k)
 let inject_if_homogenous_dependent_pair ty =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   try
+    let sigma = Tacmach.New.project gl in
     let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in
     (* fetch the informations of the  pair *)
     let ceq = Universes.constr_of_global Coqlib.glob_eq in
@@ -1310,8 +1313,8 @@ let inject_if_homogenous_dependent_pair ty =
     (* check whether the equality deals with dep pairs or not *)
     let eqTypeDest = fst (decompose_app t) in
     if not (Globnames.is_global (sigTconstr()) eqTypeDest) then raise Exit;
-    let hd1,ar1 = decompose_app_vect t1 and
-        hd2,ar2 = decompose_app_vect t2 in
+    let hd1,ar1 = decompose_app_vect sigma (EConstr.of_constr t1) and
+        hd2,ar2 = decompose_app_vect sigma (EConstr.of_constr t2) in
     if not (Globnames.is_global (existTconstr()) hd1) then raise Exit;
     if not (Globnames.is_global (existTconstr()) hd2) then raise Exit;
     let ind,_ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in
@@ -1543,7 +1546,7 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   (* We build the expected goal *)
   let abst_B =
     List.fold_right
-      (fun (e,t) body -> lambda_create env (t,subst_term e body)) e1_list b in
+      (fun (e,t) body -> lambda_create env (t,subst_term sigma (EConstr.of_constr e) (EConstr.of_constr body))) e1_list b in
   let pred_body = beta_applist(abst_B,proj_list) in
   let body = mkApp (lambda_create env (typ,pred_body),[|dep_pair1|]) in
   let expected_goal = beta_applist (abst_B,List.map fst e2_list) in
@@ -1674,8 +1677,8 @@ let is_eq_x gl x d =
     in
     let c = pf_nf_evar gl (NamedDecl.get_type d) in
     let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in
-    if (is_var x lhs) && not (local_occur_var x rhs) then raise (FoundHyp (id,rhs,true));
-    if (is_var x rhs) && not (local_occur_var x lhs) then raise (FoundHyp (id,lhs,false))
+    if (is_var x lhs) && not (local_occur_var (project gl) x (EConstr.of_constr rhs)) then raise (FoundHyp (id,rhs,true));
+    if (is_var x rhs) && not (local_occur_var (project gl) x (EConstr.of_constr lhs)) then raise (FoundHyp (id,lhs,false))
   with Constr_matching.PatternMatchingFailure ->
     ()
 
@@ -1685,6 +1688,7 @@ let is_eq_x gl x d =
 let subst_one dep_proof_ok x (hyp,rhs,dir) =
   Proofview.Goal.enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
+  let sigma = Tacmach.New.project gl in
   let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
   let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
   (* The set of hypotheses using x *)
@@ -1692,7 +1696,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
     List.rev (pi3 (List.fold_right (fun dcl (dest,deps,allhyps) ->
       let id = NamedDecl.get_id dcl in
       if not (Id.equal id hyp)
-         && List.exists (fun y -> occur_var_in_decl env y dcl) deps
+         && List.exists (fun y -> occur_var_in_decl env sigma y dcl) deps
       then
         let id_dest = if !regular_subst_tactic then dest else MoveLast in
         (dest,id::deps,(id_dest,id)::allhyps)
@@ -1701,7 +1705,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
       hyps
       (MoveBefore x,[x],[]))) in (* In practice, no dep hyps before x, so MoveBefore x is good enough *)
   (* Decides if x appears in conclusion *)
-  let depconcl = occur_var env x concl in
+  let depconcl = occur_var env sigma x (EConstr.of_constr concl) in
   let need_rewrite = not (List.is_empty dephyps) || depconcl in
   tclTHENLIST
     ((if need_rewrite then
@@ -1787,6 +1791,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
   let process hyp =
     Proofview.Goal.enter { enter = begin fun gl ->
     let gl = Proofview.Goal.assume gl in
+    let sigma = project gl in
     let env = Proofview.Goal.env gl in
     let find_eq_data_decompose = find_eq_data_decompose gl in
     let c = pf_get_hyp hyp gl |> NamedDecl.get_type in
@@ -1794,9 +1799,9 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
     (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
     if Term.eq_constr x y then Proofview.tclUNIT () else
       match kind_of_term x, kind_of_term y with
-      | Var x', _ when not (occur_term x y) && not (is_evaluable env (EvalVarRef x')) ->
+      | Var x', _ when not (occur_term sigma (EConstr.of_constr x) (EConstr.of_constr y)) && not (is_evaluable env (EvalVarRef x')) ->
           subst_one flags.rewrite_dependent_proof x' (hyp,y,true)
-      | _, Var y' when not (occur_term y x) && not (is_evaluable env (EvalVarRef y')) ->
+      | _, Var y' when not (occur_term sigma (EConstr.of_constr y) (EConstr.of_constr x)) && not (is_evaluable env (EvalVarRef y')) ->
           subst_one flags.rewrite_dependent_proof y' (hyp,x,false)
       | _ ->
           Proofview.tclUNIT ()
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 9fa49264fe..55bf5f29ea 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -45,8 +45,8 @@ type debug = Debug | Info | Off
 
 exception Bound
 
-let head_constr_bound t =
-  let t = strip_outer_cast t in
+let head_constr_bound sigma t =
+  let t = strip_outer_cast sigma (EConstr.of_constr t) in
   let _,ccl = decompose_prod_assum t in
   let hd,args = decompose_app ccl in
   match kind_of_term hd with
@@ -54,13 +54,13 @@ let head_constr_bound t =
     | Proj (p, _) -> mkConst (Projection.constant p)
     | _ -> raise Bound
 
-let head_constr c =
-  try head_constr_bound c with Bound -> error "Bound head variable."
+let head_constr sigma c =
+  try head_constr_bound sigma c with Bound -> error "Bound head variable."
 
-let decompose_app_bound t =
-  let t = strip_outer_cast t in
+let decompose_app_bound sigma t =
+  let t = strip_outer_cast sigma (EConstr.of_constr t) in
   let _,ccl = decompose_prod_assum t in
-  let hd,args = decompose_app_vect ccl in
+  let hd,args = decompose_app_vect sigma (EConstr.of_constr ccl) in
   match kind_of_term hd with
     | Const (c,u) -> ConstRef c, args
     | Ind (i,u) -> IndRef i, args
@@ -505,7 +505,7 @@ struct
 
   let match_mode m arg =
     match m with
-    | ModeInput -> not (occur_existential arg)
+    | ModeInput -> not (occur_existential Evd.empty (EConstr.of_constr arg)) (** FIXME *)
     | ModeNoHeadEvar ->
        Evarutil.(try ignore(head_evar arg); false
                  with NoHeadEvar -> true)
@@ -742,7 +742,7 @@ let secvars_of_global env gr =
 
 let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
   let secvars = secvars_of_constr env c in
-  let cty = strip_outer_cast cty in
+  let cty = strip_outer_cast sigma (EConstr.of_constr cty) in
     match kind_of_term cty with
     | Prod _ -> failwith "make_exact_entry"
     | _ ->
@@ -911,7 +911,7 @@ let make_trivial env sigma poly ?(name=PathAny) r =
   let c,ctx = fresh_global_or_constr env sigma poly r in
   let sigma = Evd.merge_context_set univ_flexible sigma ctx in
   let t = hnf_constr env sigma (unsafe_type_of env sigma c) in
-  let hd = head_of_constr_reference (head_constr t) in
+  let hd = head_of_constr_reference (head_constr sigma t) in
   let ce = mk_clenv_from_env env sigma None (c,t) in
   (Some hd, { pri=1;
 	      poly = poly;
@@ -1013,7 +1013,7 @@ let subst_autohint (subst, obj) =
   let subst_key gr =
     let (lab'', elab') = subst_global subst gr in
     let gr' =
-      (try head_of_constr_reference (head_constr_bound elab')
+      (try head_of_constr_reference (head_constr_bound Evd.empty (** FIXME *) elab')
        with Bound -> lab'')
     in if gr' == gr then gr else gr'
   in
@@ -1190,17 +1190,17 @@ let prepare_hint check (poly,local) env init (sigma,c) =
      thing make_resolves will do is to re-instantiate the products *)
   let sigma, subst = Evd.nf_univ_variables sigma in
   let c = Vars.subst_univs_constr subst (Evarutil.nf_evar sigma c) in
-  let c = drop_extra_implicit_args c in
-  let vars = ref (collect_vars c) in
+  let c = drop_extra_implicit_args sigma (EConstr.of_constr c) in
+  let vars = ref (collect_vars sigma (EConstr.of_constr c)) in
   let subst = ref [] in
   let rec find_next_evar c = match kind_of_term c with
     | Evar (evk,args as ev) ->
       (* We skip the test whether args is the identity or not *)
       let t = Evarutil.nf_evar sigma (existential_type sigma ev) in
-      let t = List.fold_right (fun (e,id) c -> replace_term e id c) !subst t in
+      let t = List.fold_right (fun (e,id) c -> replace_term sigma (EConstr.of_constr e) (EConstr.of_constr id) (EConstr.of_constr c)) !subst t in
       if not (closed0 c) then
 	error "Hints with holes dependent on a bound variable not supported.";
-      if occur_existential t then
+      if occur_existential sigma (EConstr.of_constr t) then
 	(* Not clever enough to construct dependency graph of evars *)
 	error "Not clever enough to deal with evars dependent in other evars.";
       raise (Found (c,t))
@@ -1211,7 +1211,7 @@ let prepare_hint check (poly,local) env init (sigma,c) =
       let id = next_ident_away_from default_prepare_hint_ident (fun id -> Id.Set.mem id !vars) in
       vars := Id.Set.add id !vars;
       subst := (evar,mkVar id)::!subst;
-      mkNamedLambda id t (iter (replace_term evar (mkVar id) c)) in
+      mkNamedLambda id t (iter (replace_term sigma (EConstr.of_constr evar) (EConstr.mkVar id) (EConstr.of_constr c))) in
   let c' = iter c in
     if check then Pretyping.check_evars (Global.env()) Evd.empty sigma c';
     let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
@@ -1394,13 +1394,13 @@ let pr_hint_ref ref = pr_hint_list_for_head ref
 
 (* Print all hints associated to head id in any database *)
 
-let pr_hint_term cl =
+let pr_hint_term sigma cl =
   try
     let dbs = current_db () in
     let valid_dbs =
       let fn = try
-	  let hdc = decompose_app_bound cl in
-	    if occur_existential cl then
+	  let hdc = decompose_app_bound sigma cl in
+	    if occur_existential sigma (EConstr.of_constr cl) then
 	      Hint_db.map_existential ~secvars:Id.Pred.full hdc cl
 	    else Hint_db.map_auto ~secvars:Id.Pred.full hdc cl
 	with Bound -> Hint_db.map_none ~secvars:Id.Pred.full
@@ -1423,7 +1423,7 @@ let pr_applicable_hint () =
   match glss.Evd.it with
   | [] -> CErrors.error "No focused goal."
   | g::_ ->
-    pr_hint_term (Goal.V82.concl glss.Evd.sigma g)
+    pr_hint_term glss.Evd.sigma (Goal.V82.concl glss.Evd.sigma g)
 
 let pp_hint_mode = function
   | ModeInput -> str"+"
diff --git a/tactics/hints.mli b/tactics/hints.mli
index edc65c4070..c0eb2c3b86 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -24,7 +24,7 @@ open Vernacexpr
 
 exception Bound
 
-val decompose_app_bound : constr -> global_reference * constr array
+val decompose_app_bound : evar_map -> constr -> global_reference * constr array
 
 type debug = Debug | Info | Off
 
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 27af7200bd..847ecf4b0e 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -31,9 +31,9 @@ module RelDecl = Context.Rel.Declaration
 
   -- Eduardo (6/8/97). *)
 
-type 'a matching_function = constr -> 'a option
+type 'a matching_function = Evd.evar_map -> constr -> 'a option
 
-type testing_function  = constr -> bool
+type testing_function  = Evd.evar_map -> constr -> bool
 
 let mkmeta n = Nameops.make_ident "X" (Some n)
 let meta1 = mkmeta 1
@@ -43,7 +43,7 @@ let meta4 = mkmeta 4
 
 let op2bool = function Some _ -> true | None -> false
 
-let match_with_non_recursive_type t =
+let match_with_non_recursive_type sigma t =
   match kind_of_term t with
     | App _ ->
         let (hdapp,args) = decompose_app t in
@@ -56,21 +56,21 @@ let match_with_non_recursive_type t =
            | _ -> None)
     | _ -> None
 
-let is_non_recursive_type t = op2bool (match_with_non_recursive_type t)
+let is_non_recursive_type sigma t = op2bool (match_with_non_recursive_type sigma t)
 
 (* Test dependencies *)
 
 (* NB: we consider also the let-in case in the following function,
    since they may appear in types of inductive constructors (see #2629) *)
 
-let rec has_nodep_prod_after n c =
+let rec has_nodep_prod_after n sigma c =
   match kind_of_term c with
     | Prod (_,_,b) | LetIn (_,_,_,b) ->
-	( n>0 || not (dependent (mkRel 1) b))
-	&& (has_nodep_prod_after (n-1) b)
+	( n>0 || EConstr.Vars.noccurn sigma 1 (EConstr.of_constr b))
+	&& (has_nodep_prod_after (n-1) sigma b)
     | _            -> true
 
-let has_nodep_prod = has_nodep_prod_after 0
+let has_nodep_prod sigma c = has_nodep_prod_after 0 sigma c
 
 (* A general conjunctive type is a non-recursive with-no-indices inductive
    type with only one constructor and no dependencies between argument;
@@ -87,7 +87,7 @@ let is_lax_conjunction = function
 | Some false -> true
 | _ -> false
 
-let match_with_one_constructor style onlybinary allow_rec t =
+let match_with_one_constructor sigma style onlybinary allow_rec t =
   let (hdapp,args) = decompose_app t in
   let res = match kind_of_term hdapp with
   | Ind ind ->
@@ -112,7 +112,7 @@ let match_with_one_constructor style onlybinary allow_rec t =
 	else
 	  let ctyp = prod_applist mip.mind_nf_lc.(0) args in
 	  let cargs = List.map RelDecl.get_type (prod_assum ctyp) in
-	  if not (is_lax_conjunction style) || has_nodep_prod ctyp then
+	  if not (is_lax_conjunction style) || has_nodep_prod sigma ctyp then
 	    (* Record or non strict conjunction *)
 	    Some (hdapp,List.rev cargs)
 	  else
@@ -125,28 +125,28 @@ let match_with_one_constructor style onlybinary allow_rec t =
   | Some (hdapp, [_; _]) -> res
   | _ -> None
 
-let match_with_conjunction ?(strict=false) ?(onlybinary=false) t =
-  match_with_one_constructor (Some strict) onlybinary false t
+let match_with_conjunction ?(strict=false) ?(onlybinary=false) sigma t =
+  match_with_one_constructor sigma (Some strict) onlybinary false t
 
-let match_with_record t =
-  match_with_one_constructor None false false t
+let match_with_record sigma t =
+  match_with_one_constructor sigma None false false t
 
-let is_conjunction ?(strict=false) ?(onlybinary=false) t =
-  op2bool (match_with_conjunction ~strict ~onlybinary t)
+let is_conjunction ?(strict=false) ?(onlybinary=false) sigma t =
+  op2bool (match_with_conjunction sigma ~strict ~onlybinary t)
 
-let is_record t =
-  op2bool (match_with_record t)
+let is_record sigma t =
+  op2bool (match_with_record sigma t)
 
-let match_with_tuple t =
-  let t = match_with_one_constructor None false true t in
+let match_with_tuple sigma t =
+  let t = match_with_one_constructor sigma None false true t in
   Option.map (fun (hd,l) ->
     let ind = destInd hd in
     let (mib,mip) = Global.lookup_pinductive ind in
     let isrec = mis_is_recursive (fst ind,mib,mip) in
     (hd,l,isrec)) t
 
-let is_tuple t =
-  op2bool (match_with_tuple t)
+let is_tuple sigma t =
+  op2bool (match_with_tuple sigma t)
 
 (* A general disjunction type is a non-recursive with-no-indices inductive
    type with of which all constructors have a single argument;
@@ -159,7 +159,7 @@ let test_strict_disjunction n lc =
     | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i)
     | _ -> false) 0 lc
 
-let match_with_disjunction ?(strict=false) ?(onlybinary=false) t =
+let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t =
   let (hdapp,args) = decompose_app t in
   let res = match kind_of_term hdapp with
   | Ind (ind,u)  ->
@@ -187,13 +187,13 @@ let match_with_disjunction ?(strict=false) ?(onlybinary=false) t =
   | Some (hdapp,[_; _]) -> res
   | _ -> None
 
-let is_disjunction ?(strict=false) ?(onlybinary=false) t =
-  op2bool (match_with_disjunction ~strict ~onlybinary t)
+let is_disjunction ?(strict=false) ?(onlybinary=false) sigma t =
+  op2bool (match_with_disjunction ~strict ~onlybinary sigma t)
 
 (* An empty type is an inductive type, possible with indices, that has no
    constructors *)
 
-let match_with_empty_type t =
+let match_with_empty_type sigma t =
   let (hdapp,args) = decompose_app t in
   match (kind_of_term hdapp) with
     | Ind ind ->
@@ -202,33 +202,33 @@ let match_with_empty_type t =
 	if Int.equal nconstr 0 then Some hdapp else None
     | _ ->  None
 
-let is_empty_type t = op2bool (match_with_empty_type t)
+let is_empty_type sigma t = op2bool (match_with_empty_type sigma t)
 
 (* This filters inductive types with one constructor with no arguments;
    Parameters and indices are allowed *)
 
-let match_with_unit_or_eq_type t =
+let match_with_unit_or_eq_type sigma t =
   let (hdapp,args) = decompose_app t in
   match (kind_of_term hdapp) with
     | Ind ind  ->
         let (mib,mip) = Global.lookup_pinductive ind in
         let constr_types = mip.mind_nf_lc in
         let nconstr = Array.length mip.mind_consnames in
-        let zero_args c = Int.equal (nb_prod c) mib.mind_nparams in
+        let zero_args c = Int.equal (nb_prod sigma (EConstr.of_constr c)) mib.mind_nparams in
 	if Int.equal nconstr 1 && zero_args constr_types.(0) then
 	  Some hdapp
 	else
 	  None
     | _ -> None
 
-let is_unit_or_eq_type t = op2bool (match_with_unit_or_eq_type t)
+let is_unit_or_eq_type sigma t = op2bool (match_with_unit_or_eq_type sigma t)
 
 (* A unit type is an inductive type with no indices but possibly
    (useless) parameters, and that has no arguments in its unique
    constructor *)
 
-let is_unit_type t =
-  match match_with_conjunction t with
+let is_unit_type sigma t =
+  match match_with_conjunction sigma t with
   | Some (_,[]) -> true
   | _ -> false
 
@@ -318,13 +318,13 @@ let is_inductive_equality ind =
   let nconstr = Array.length mip.mind_consnames in
   Int.equal nconstr 1 && Int.equal (constructor_nrealargs (ind,1)) 0
 
-let match_with_equality_type t =
+let match_with_equality_type sigma t =
   let (hdapp,args) = decompose_app t in
   match (kind_of_term hdapp) with
   | Ind (ind,_) when is_inductive_equality ind -> Some (hdapp,args)
   | _ -> None
 
-let is_equality_type t = op2bool (match_with_equality_type t)
+let is_equality_type sigma t = op2bool (match_with_equality_type sigma t)
 
 (* Arrows/Implication/Negation *)
 
@@ -338,37 +338,37 @@ let match_arrow_pattern t =
       assert (Id.equal m1 meta1 && Id.equal m2 meta2); (arg, mind)
     | _ -> anomaly (Pp.str "Incorrect pattern matching")
 
-let match_with_imp_term c=
+let match_with_imp_term sigma c =
   match kind_of_term c with
-    | Prod (_,a,b) when not (dependent (mkRel 1) b) ->Some (a,b)
+    | Prod (_,a,b) when EConstr.Vars.noccurn sigma 1 (EConstr.of_constr b) -> Some (a,b)
     | _              -> None
 
-let is_imp_term c = op2bool (match_with_imp_term c)
+let is_imp_term sigma c = op2bool (match_with_imp_term sigma c)
 
-let match_with_nottype t =
+let match_with_nottype sigma t =
   try
     let (arg,mind) = match_arrow_pattern t in
-    if is_empty_type mind then Some (mind,arg) else None
+    if is_empty_type sigma mind then Some (mind,arg) else None
   with PatternMatchingFailure -> None
 
-let is_nottype t = op2bool (match_with_nottype t)
+let is_nottype sigma t = op2bool (match_with_nottype sigma t)
 
 (* Forall *)
 
-let match_with_forall_term c=
+let match_with_forall_term sigma c=
   match kind_of_term c with
     | Prod (nam,a,b) -> Some (nam,a,b)
     | _            -> None
 
-let is_forall_term c = op2bool (match_with_forall_term c)
+let is_forall_term sigma c = op2bool (match_with_forall_term sigma c)
 
-let match_with_nodep_ind t =
+let match_with_nodep_ind sigma t =
   let (hdapp,args) = decompose_app t in
     match (kind_of_term hdapp) with
       | Ind ind  ->
           let (mib,mip) = Global.lookup_pinductive ind in
 	    if Array.length (mib.mind_packets)>1 then None else
-	      let nodep_constr = has_nodep_prod_after mib.mind_nparams in
+	      let nodep_constr = has_nodep_prod_after mib.mind_nparams sigma in
 		if Array.for_all nodep_constr mip.mind_nf_lc then
 		  let params=
 		    if Int.equal mip.mind_nrealargs 0 then args else
@@ -378,9 +378,9 @@ let match_with_nodep_ind t =
 		  None
       | _ -> None
 
-let is_nodep_ind t=op2bool (match_with_nodep_ind t)
+let is_nodep_ind sigma t = op2bool (match_with_nodep_ind sigma t)
 
-let match_with_sigma_type t=
+let match_with_sigma_type sigma t =
   let (hdapp,args) = decompose_app t in
   match (kind_of_term hdapp) with
     | Ind ind  ->
@@ -388,14 +388,14 @@ let match_with_sigma_type t=
           if Int.equal (Array.length (mib.mind_packets)) 1 &&
 	    (Int.equal mip.mind_nrealargs 0) &&
 	    (Int.equal (Array.length mip.mind_consnames)1) &&
-	    has_nodep_prod_after (mib.mind_nparams+1) mip.mind_nf_lc.(0) then
+	    has_nodep_prod_after (mib.mind_nparams+1) sigma mip.mind_nf_lc.(0) then
 	      (*allowing only 1 existential*)
 	      Some (hdapp,args)
 	  else
 	    None
     | _ -> None
 
-let is_sigma_type t=op2bool (match_with_sigma_type t)
+let is_sigma_type sigma t = op2bool (match_with_sigma_type sigma t)
 
 (***** Destructing patterns bound to some theory *)
 
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 7cc41f1b93..8a453bf31f 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -40,8 +40,8 @@ open Coqlib
    also work on ad-hoc disjunctions introduced by the user.
    (Eduardo, 6/8/97). *)
 
-type 'a matching_function = constr -> 'a option
-type testing_function = constr -> bool
+type 'a matching_function = Evd.evar_map -> constr -> 'a option
+type testing_function = Evd.evar_map -> constr -> bool
 
 val match_with_non_recursive_type : (constr * constr list) matching_function
 val is_non_recursive_type         : testing_function
diff --git a/tactics/inv.ml b/tactics/inv.ml
index e7d8249e43..d1d6178da2 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -32,8 +32,9 @@ module NamedDecl = Context.Named.Declaration
 
 let var_occurs_in_pf gl id =
   let env = Proofview.Goal.env gl in
-  occur_var env id (Proofview.Goal.concl gl) ||
-  List.exists (occur_var_in_decl env id) (Proofview.Goal.hyps gl)
+  let sigma = project gl in
+  occur_var env sigma id (EConstr.of_constr (Proofview.Goal.concl gl)) ||
+  List.exists (occur_var_in_decl env sigma id) (Proofview.Goal.hyps gl)
 
 (* [make_inv_predicate (ity,args) C]
 
@@ -75,7 +76,7 @@ let make_inv_predicate env evd indf realargs id status concl =
 	  let hyps_arity,_ = get_arity env indf in
 	    (hyps_arity,concl)
       | Dep dflt_concl ->
-	  if not (occur_var env id concl) then
+	  if not (occur_var env !evd id (EConstr.of_constr concl)) then
 	    user_err ~hdr:"make_inv_predicate"
               (str "Current goal does not depend on " ++ pr_id id ++ str".");
           (* We abstract the conclusion of goal with respect to
@@ -183,7 +184,7 @@ let dependent_hyps env id idlist gl =
     | d::l ->
 	(* Update the type of id1: it may have been subject to rewriting *)
 	let d = pf_get_hyp (NamedDecl.get_id d) gl in
-	if occur_var_in_decl env id d
+	if occur_var_in_decl env (project gl) id d
         then d :: dep_rec l
         else dep_rec l
   in
@@ -448,7 +449,7 @@ let raw_inversion inv_kind id status names =
       make_inv_predicate env evdref indf realargs id status concl in
     let sigma = !evdref in
     let (cut_concl,case_tac) =
-      if status != NoDep && (dependent c concl) then
+      if status != NoDep && (dependent sigma (EConstr.of_constr c) (EConstr.of_constr concl)) then
         Reduction.beta_appvect elim_predicate (Array.of_list (realargs@[c])),
         case_then_using
       else
@@ -514,12 +515,14 @@ let invIn k names ids id =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let hyps = List.map (fun id -> pf_get_hyp id gl) ids in
     let concl = Proofview.Goal.concl gl in
-    let nb_prod_init = nb_prod concl in
+    let sigma = project gl in
+    let nb_prod_init = nb_prod sigma (EConstr.of_constr concl) in
     let intros_replace_ids =
       Proofview.Goal.enter { enter = begin fun gl ->
         let concl = pf_nf_concl gl in
+        let sigma = project gl in
         let nb_of_new_hyp =
-          nb_prod concl - (List.length hyps + nb_prod_init)
+          nb_prod sigma (EConstr.of_constr concl) - (List.length hyps + nb_prod_init)
         in
         if nb_of_new_hyp < 1 then
           intros_replacing ids
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 10fc5076c2..46f1f7c8d0 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -154,7 +154,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
       pty,goal
     else
       let i = mkAppliedInd ind in
-      let ivars = global_vars env i in
+      let ivars = global_vars env sigma (EConstr.of_constr i) in
       let revargs,ownsign =
 	fold_named_context
 	  (fun env d (revargs,hyps) ->
@@ -192,7 +192,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   in
   assert
     (List.subset
-       (global_vars env invGoal)
+       (global_vars env sigma (EConstr.of_constr invGoal))
        (ids_of_named_context (named_context invEnv)));
   (*
     user_err ~hdr:"lemma_inversion"
@@ -277,7 +277,8 @@ let lemInvIn id c ids =
     let hyps = List.map (fun id -> pf_get_hyp id gl) ids in
     let intros_replace_ids =
       let concl = Proofview.Goal.concl gl in
-      let nb_of_new_hyp  = nb_prod concl - List.length ids in
+      let sigma = project gl in
+      let nb_of_new_hyp = nb_prod sigma (EConstr.of_constr concl) - List.length ids in
       if nb_of_new_hyp < 1  then
         intros_replacing ids
       else
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 93c04e373c..676b23d095 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -630,7 +630,7 @@ module New = struct
     (* applying elimination_scheme just a little modified *)
     let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl elim)) gl in
     let indmv =
-      match kind_of_term (last_arg elimclause.templval.Evd.rebus) with
+      match kind_of_term (last_arg elimclause.evd (EConstr.of_constr elimclause.templval.Evd.rebus)) with
       | Meta mv -> mv
       | _         -> anomaly (str"elimination")
     in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e17bbfcb06..15dd1a97ce 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -323,10 +323,11 @@ let apply_clear_request clear_flag dft c =
 let move_hyp id dest =
   Proofview.Goal.enter { enter = begin fun gl ->
     let env = Proofview.Goal.env gl in
+    let sigma = Tacmach.New.project gl in
     let ty = Proofview.Goal.raw_concl gl in
     let store = Proofview.Goal.extra gl in
     let sign = named_context_val env in
-    let sign' = move_hyp_in_named_context id dest sign in
+    let sign' = move_hyp_in_named_context sigma id dest sign in
     let env = reset_with_named_context sign' env in
     Refine.refine ~unsafe:true { run = begin fun sigma ->
       Evarutil.new_evar env sigma ~principal:true ~store ty
@@ -497,7 +498,7 @@ fun env sigma p -> function
   let Sigma (rem, sigma, r) = mk_holes env sigma (p +> q) rem in
   Sigma (arg :: rem, sigma, r)
 
-let rec check_mutind env sigma k cl = match kind_of_term (strip_outer_cast cl) with
+let rec check_mutind env sigma k cl = match kind_of_term (strip_outer_cast sigma (EConstr.of_constr cl)) with
 | Prod (na, c1, b) ->
   if Int.equal k 1 then
     try
@@ -936,13 +937,14 @@ let build_intro_tac id dest tac = match dest with
 let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
   let open Context.Rel.Declaration in
   Proofview.Goal.enter { enter = begin fun gl ->
+    let sigma = Tacmach.New.project gl in
     let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
     let concl = nf_evar (Tacmach.New.project gl) concl in
     match kind_of_term concl with
-    | Prod (name,t,u) when not dep_flag || (dependent (mkRel 1) u) ->
+    | Prod (name,t,u) when not dep_flag || not (EConstr.Vars.noccurn sigma 1 (EConstr.of_constr u)) ->
         let name = find_name false (LocalAssum (name,t)) name_flag gl in
 	build_intro_tac name move_flag tac
-    | LetIn (name,b,t,u) when not dep_flag || (dependent (mkRel 1) u) ->
+    | LetIn (name,b,t,u) when not dep_flag || not (EConstr.Vars.noccurn sigma 1 (EConstr.of_constr u)) ->
         let name = find_name false (LocalDef (name,b,t)) name_flag gl in
 	build_intro_tac name move_flag tac
     | _ ->
@@ -1285,7 +1287,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true)
   in
   let new_hyp_typ = clenv_type clenv in
   if not with_evars then check_unresolved_evars_of_metas sigma0 clenv;
-  if not with_evars && occur_meta new_hyp_typ then
+  if not with_evars && occur_meta clenv.evd (EConstr.of_constr new_hyp_typ) then
     error_uninstantiated_metas new_hyp_typ clenv;
   let new_hyp_prf = clenv_value clenv in
   let exact_tac = Proofview.V82.tactic (Tacmach.refine_no_check new_hyp_prf) in
@@ -1440,7 +1442,7 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) =
   let (mind,_) = reduce_to_quantified_ind env (Sigma.to_evar_map sigma) t in
   let sort = Tacticals.New.elimination_sort_of_goal gl in
   let Sigma (elim, sigma, p) =
-    if occur_term c concl then
+    if occur_term (Sigma.to_evar_map sigma) (EConstr.of_constr c) (EConstr.of_constr concl) then
       build_case_analysis_scheme env sigma mind true sort
     else
       build_case_analysis_scheme_default env sigma mind sort in
@@ -1624,7 +1626,7 @@ let descend_in_conjunctions avoid tac (err, info) c =
     let t = Retyping.get_type_of env sigma c in
     let ((ind,u),t) = reduce_to_quantified_ind env sigma t in
     let sign,ccl = decompose_prod_assum t in
-    match match_with_tuple ccl with
+    match match_with_tuple sigma ccl with
     | Some (_,_,isrec) ->
 	let n = (constructors_nrealargs ind).(0) in
 	let sort = Tacticals.New.elimination_sort_of_goal gl in
@@ -1689,12 +1691,13 @@ let tclORELSEOPT t k =
 let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   let concl = Proofview.Goal.concl gl in
+  let sigma = Tacmach.New.project gl in
   let flags =
     if with_delta then default_unify_flags () else default_no_delta_unify_flags () in
   (* The actual type of the theorem. It will be matched against the
   goal. If this fails, then the head constant will be unfolded step by
   step. *)
-  let concl_nprod = nb_prod_modulo_zeta concl in
+  let concl_nprod = nb_prod_modulo_zeta sigma (EConstr.of_constr concl) in
   let rec try_main_apply with_destruct c =
     Proofview.Goal.enter { enter = begin fun gl ->
     let env = Proofview.Goal.env gl in
@@ -1703,7 +1706,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind))
     let thm_ty0 = nf_betaiota sigma (Retyping.get_type_of env sigma c) in
     let try_apply thm_ty nprod =
       try
-        let n = nb_prod_modulo_zeta thm_ty - nprod in
+        let n = nb_prod_modulo_zeta sigma (EConstr.of_constr thm_ty) - nprod in
         if n<0 then error "Applied theorem has not enough premisses.";
         let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in
         Clenvtac.res_pf clause ~with_evars ~flags
@@ -1901,8 +1904,9 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam
 
 let cut_and_apply c =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
+    let sigma = Tacmach.New.project gl in
     match kind_of_term (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_unsafe_type_of gl c)) with
-      | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) ->
+      | Prod (_,c1,c2) when EConstr.Vars.noccurn sigma 1 (EConstr.of_constr c2) ->
         let concl = Proofview.Goal.concl gl in
         let env = Tacmach.New.pf_env gl in
         Refine.refine { run = begin fun sigma ->
@@ -2049,7 +2053,7 @@ let clear_body ids =
           (** Do no recheck hypotheses that do not depend *)
           let sigma =
             if not seen then sigma
-            else if List.exists (fun id -> occur_var_in_decl env id decl) ids then
+            else if List.exists (fun id -> occur_var_in_decl env sigma id decl) ids then
               check_decl env sigma decl
             else sigma
           in
@@ -2058,7 +2062,7 @@ let clear_body ids =
         in
         let (env, sigma, _) = List.fold_left check (base_env, sigma, false) (List.rev ctx) in
         let sigma =
-          if List.exists (fun id -> occur_var env id concl) ids then
+          if List.exists (fun id -> occur_var env sigma id (EConstr.of_constr concl)) ids then
             check_is_type env sigma concl
           else sigma
         in
@@ -2096,12 +2100,13 @@ let keep hyps =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   Proofview.tclENV >>= fun env ->
   let ccl = Proofview.Goal.concl gl in
+  let sigma = Tacmach.New.project gl in
   let cl,_ =
     fold_named_context_reverse (fun (clear,keep) decl ->
       let hyp = NamedDecl.get_id decl in
       if Id.List.mem hyp hyps
-        || List.exists (occur_var_in_decl env hyp) keep
-	|| occur_var env hyp ccl
+        || List.exists (occur_var_in_decl env sigma hyp) keep
+	|| occur_var env sigma hyp (EConstr.of_constr ccl)
       then (clear,decl::keep)
       else (hyp::clear,keep))
       ~init:([],[]) (Proofview.Goal.env gl)
@@ -2310,15 +2315,16 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac =
     List.filter (fun (_,id) -> not (Id.equal id id')) thin in
   Proofview.Goal.enter { enter = begin fun gl ->
     let env = Proofview.Goal.env gl in
+    let sigma = Tacmach.New.project gl in
     let type_of = Tacmach.New.pf_unsafe_type_of gl in
     let whd_all = Tacmach.New.pf_apply whd_all gl in
     let t = whd_all (type_of (mkVar id)) in
-    let eqtac, thin = match match_with_equality_type t with
+    let eqtac, thin = match match_with_equality_type sigma t with
     | Some (hdcncl,[_;lhs;rhs]) ->
-        if l2r && isVar lhs && not (occur_var env (destVar lhs) rhs) then
+        if l2r && isVar lhs && not (occur_var env sigma (destVar lhs) (EConstr.of_constr rhs)) then
           let id' = destVar lhs in
           subst_on l2r id' rhs, early_clear id' thin
-        else if not l2r && isVar rhs && not (occur_var env (destVar rhs) lhs) then
+        else if not l2r && isVar rhs && not (occur_var env sigma (destVar rhs) (EConstr.of_constr lhs)) then
           let id' = destVar rhs in
           subst_on l2r id' lhs, early_clear id' thin
         else
@@ -2763,8 +2769,8 @@ let generalized_name c t ids cl = function
 let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl =
   let open Context.Rel.Declaration in
   let decls,cl = decompose_prod_n_assum i cl in
-  let dummy_prod = it_mkProd_or_LetIn mkProp decls in
-  let newdecls,_ = decompose_prod_n_assum i (subst_term_gen eq_constr_nounivs c dummy_prod) in
+  let dummy_prod = EConstr.of_constr (it_mkProd_or_LetIn mkProp decls) in
+  let newdecls,_ = decompose_prod_n_assum i (subst_term_gen sigma EConstr.eq_constr_nounivs (EConstr.of_constr c) dummy_prod) in
   let cl',sigma' = subst_closed_term_occ env sigma (AtOccs occs) c (it_mkProd_or_LetIn cl newdecls) in
   let na = generalized_name c t ids cl' na in
   let decl = match b with
@@ -2782,10 +2788,11 @@ let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) =
 let old_generalize_dep ?(with_let=false) c gl =
   let env = pf_env gl in
   let sign = pf_hyps gl in
+  let sigma = project gl in
   let init_ids = ids_of_named_context (Global.named_context()) in
   let seek (d:Context.Named.Declaration.t) (toquant:Context.Named.t) =
-    if List.exists (fun d' -> occur_var_in_decl env (NamedDecl.get_id d') d) toquant
-      || dependent_in_decl c d then
+    if List.exists (fun d' -> occur_var_in_decl env sigma (NamedDecl.get_id d') d) toquant
+      || dependent_in_decl sigma (EConstr.of_constr c) d then
       d::toquant
     else
       toquant in
@@ -2901,14 +2908,14 @@ let specialize (c,lbind) ipat =
       let (thd,tstack) = whd_nored_stack clause.evd (clenv_value clause) in
       let rec chk = function
       | [] -> []
-      | t::l -> if occur_meta t then [] else t :: chk l
+      | t::l -> if occur_meta clause.evd (EConstr.of_constr t) then [] else t :: chk l
       in
       let tstack = chk tstack in
       let term = applist(thd,List.map (nf_evar clause.evd) tstack) in
-      if occur_meta term then
+      if occur_meta clause.evd (EConstr.of_constr term) then
 	user_err  (str "Cannot infer an instance for " ++
 
-          pr_name (meta_name clause.evd (List.hd (collect_metas term))) ++
+          pr_name (meta_name clause.evd (List.hd (collect_metas clause.evd (EConstr.of_constr term)))) ++
 	  str ".");
       clause.evd, term in
   let typ = Retyping.get_type_of env sigma term in
@@ -3143,10 +3150,11 @@ let induct_discharge with_evars dests avoid' tac (avoid,ra) names =
 let expand_projections env sigma c =
   let sigma = Sigma.to_evar_map sigma in
   let rec aux env c =
-    match kind_of_term c with
-    | Proj (p, c) -> Retyping.expand_projection env sigma p (aux env c) []
-    | _ -> map_constr_with_full_binders push_rel aux env c
-  in aux env c
+    match EConstr.kind sigma c with
+    | Proj (p, c) -> EConstr.of_constr (Retyping.expand_projection env sigma p (EConstr.Unsafe.to_constr (aux env c)) [])
+    | _ -> map_constr_with_full_binders sigma push_rel aux env c
+  in
+  EConstr.Unsafe.to_constr (aux env (EConstr.of_constr c))
 			       
 	   
 (* Marche pas... faut prendre en compte l'occurrence précise... *)
@@ -3173,16 +3181,17 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
     else
       let c = List.nth argl (i-1) in
       match kind_of_term c with
-	| Var id when not (List.exists (occur_var env id) args') &&
-                      not (List.exists (occur_var env id) params') ->
+	| Var id when not (List.exists (fun c -> occur_var env (Sigma.to_evar_map sigma) id (EConstr.of_constr c)) args') &&
+                      not (List.exists (fun c -> occur_var env (Sigma.to_evar_map sigma) id (EConstr.of_constr c)) params') ->
             (* Based on the knowledge given by the user, all
                constraints on the variable are generalizable in the
                current environment so that it is clearable after destruction *)
 	    atomize_one (i-1) (c::args) (c::args') (id::avoid)
 	| _ ->
 	   let c' = expand_projections env' sigma c in
-            if List.exists (dependent c) params' ||
-               List.exists (dependent c) args'
+            let dependent t = dependent (Sigma.to_evar_map sigma) (EConstr.of_constr c) (EConstr.of_constr t) in
+            if List.exists dependent params' ||
+               List.exists dependent args'
             then
               (* This is a case where the argument is constrained in a
                  way which would require some kind of inversion; we
@@ -3272,7 +3281,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
 
 exception Shunt of Id.t move_location
 
-let cook_sign hyp0_opt inhyps indvars env =
+let cook_sign hyp0_opt inhyps indvars env sigma =
   (* First phase from L to R: get [toclear], [decldep] and [statuslist]
      for the hypotheses before (= more ancient than) hyp0 (see above) *)
   let toclear = ref [] in
@@ -3299,11 +3308,11 @@ let cook_sign hyp0_opt inhyps indvars env =
       rhyp
     end else
       let dephyp0 = List.is_empty inhyps && 
-	(Option.cata (fun id -> occur_var_in_decl env id decl) false hyp0_opt)
+	(Option.cata (fun id -> occur_var_in_decl env sigma id decl) false hyp0_opt)
       in
       let depother = List.is_empty inhyps &&
-	(List.exists (fun id -> occur_var_in_decl env id decl) indvars ||
-         List.exists (fun decl' -> occur_var_in_decl env (NamedDecl.get_id decl') decl) !decldeps)
+	(List.exists (fun id -> occur_var_in_decl env sigma id decl) indvars ||
+         List.exists (fun decl' -> occur_var_in_decl env sigma (NamedDecl.get_id decl') decl) !decldeps)
       in
       if not (List.is_empty inhyps) && Id.List.mem hyp inhyps
          || dephyp0 || depother
@@ -3549,7 +3558,7 @@ let make_abstract_generalize env id typ concl dep ctx body c eqs args refls =
   Sigma (mkApp (appeqs, abshypt), sigma, p)
   end }
 
-let hyps_of_vars env sign nogen hyps =
+let hyps_of_vars env sigma sign nogen hyps =
   if Id.Set.is_empty hyps then []
   else
     let (_,lh) =
@@ -3559,7 +3568,7 @@ let hyps_of_vars env sign nogen hyps =
 	  if Id.Set.mem x nogen then (hs,hl)
 	  else if Id.Set.mem x hs then (hs,x::hl)
 	  else
-	    let xvars = global_vars_set_of_decl env d in
+	    let xvars = global_vars_set_of_decl env sigma d in
 	      if not (Id.Set.is_empty (Id.Set.diff xvars hs)) then
 		(Id.Set.add x hs, x :: hl)
 	      else (hs, hl))
@@ -3592,7 +3601,7 @@ let abstract_args gl generalize_vars dep id defined f args =
   let sigma = ref (Tacmach.project gl) in
   let env = Tacmach.pf_env gl in
   let concl = Tacmach.pf_concl gl in
-  let dep = dep || dependent (mkVar id) concl in
+  let dep = dep || local_occur_var !sigma id (EConstr.of_constr concl) in
   let avoid = ref [] in
   let get_id name =
     let id = fresh_id !avoid (match name with Name n -> n | Anonymous -> Id.of_string "gen_x") gl in
@@ -3659,7 +3668,7 @@ let abstract_args gl generalize_vars dep id defined f args =
       let vars =
 	if generalize_vars then
 	  let nogen = Id.Set.add id nogen in
-	    hyps_of_vars (pf_env gl) (pf_hyps gl) nogen vars
+	    hyps_of_vars (pf_env gl) (project gl) (pf_hyps gl) nogen vars
 	else []
       in
       let body, c' =
@@ -3845,7 +3854,7 @@ let compute_elim_sig ?elimc elimt =
 
   let ccl = exchange_hd_app (mkVar (Id.of_string "__QI_DUMMY__")) conclusion in
   let concl_with_args = it_mkProd_or_LetIn ccl args_indargs in
-  let nparams = Int.Set.cardinal (free_rels concl_with_args) in
+  let nparams = Int.Set.cardinal (free_rels Evd.empty (** FIXME *) (EConstr.of_constr concl_with_args)) in
   let preds,params = List.chop (List.length params_preds - nparams) params_preds in
 
   (* A first approximation, further analysis will tweak it *)
@@ -3905,7 +3914,7 @@ let compute_elim_sig ?elimc elimt =
 	  with e when CErrors.noncritical e ->
             error "Cannot find the inductive type of the inductive scheme."
 
-let compute_scheme_signature scheme names_info ind_type_guess =
+let compute_scheme_signature evd scheme names_info ind_type_guess =
   let open Context.Rel.Declaration in
   let f,l = decompose_app scheme.concl in
   (* Vérifier que les arguments de Qi sont bien les xi. *)
@@ -3940,9 +3949,9 @@ let compute_scheme_signature scheme names_info ind_type_guess =
   let rec check_branch p c =
     match kind_of_term c with
       | Prod (_,t,c) ->
-	(is_pred p t, true, dependent (mkRel 1) c) :: check_branch (p+1) c
+	(is_pred p t, true, not (EConstr.Vars.noccurn evd 1 (EConstr.of_constr c))) :: check_branch (p+1) c
       | LetIn (_,_,_,c) ->
-	(OtherArg, false, dependent (mkRel 1) c) :: check_branch (p+1) c
+	(OtherArg, false, not (EConstr.Vars.noccurn evd 1 (EConstr.of_constr c))) :: check_branch (p+1) c
       | _ when is_pred p c == IndArg -> []
       | _ -> raise Exit
   in
@@ -3975,7 +3984,7 @@ let compute_scheme_signature scheme names_info ind_type_guess =
    different. *)
 let compute_elim_signature (evd,(elimc,elimt),ind_type_guess) names_info =
   let scheme = compute_elim_sig ~elimc:elimc elimt in
-    evd, (compute_scheme_signature scheme names_info ind_type_guess, scheme)
+    evd, (compute_scheme_signature evd scheme names_info ind_type_guess, scheme)
 
 let guess_elim isrec dep s hyp0 gl =
   let tmptyp0 =	Tacmach.New.pf_get_hyp_typ hyp0 gl in
@@ -4022,7 +4031,7 @@ let find_induction_type isrec elim hyp0 gl =
 	let evd, (elimc,elimt),ind_guess = given_elim hyp0 e gl in
 	let scheme = compute_elim_sig ~elimc elimt in
 	if Option.is_empty scheme.indarg then error "Cannot find induction type";
-	let indsign = compute_scheme_signature scheme hyp0 ind_guess in
+	let indsign = compute_scheme_signature evd scheme hyp0 ind_guess in
 	let elim = ({elimindex = Some(-1); elimbody = elimc; elimrename = None},elimt) in
 	scheme, ElimUsing (elim,indsign)
   in
@@ -4049,7 +4058,7 @@ let get_eliminator elim dep s gl =
   | ElimOver (isrec,id) ->
       let evd, (elimc,elimt),_ as elims = guess_elim isrec dep s id gl in
       let _, (l, s) = compute_elim_signature elims id in
-      let branchlengthes = List.map (fun d -> assert (RelDecl.is_local_assum d); pi1 (decompose_prod_letin (RelDecl.get_type d)))
+      let branchlengthes = List.map (fun d -> assert (RelDecl.is_local_assum d); pi1 (decompose_prod_letin (Tacmach.New.project gl) (EConstr.of_constr (RelDecl.get_type d))))
                                     (List.rev s.branches)
       in
       evd, isrec, ({elimindex = None; elimbody = elimc; elimrename = Some (isrec,Array.of_list branchlengthes)}, elimt), l
@@ -4118,8 +4127,8 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_
     let env = Proofview.Goal.env gl in
     let sigma = Sigma.to_evar_map sigma in
     let concl = Tacmach.New.pf_nf_concl gl in
-    let statuslists,lhyp0,toclear,deps,avoid,dep_in_hyps = cook_sign hyp0 inhyps indvars env in
-    let dep_in_concl = Option.cata (fun id -> occur_var env id concl) false hyp0 in
+    let statuslists,lhyp0,toclear,deps,avoid,dep_in_hyps = cook_sign hyp0 inhyps indvars env sigma in
+    let dep_in_concl = Option.cata (fun id -> occur_var env sigma id (EConstr.of_constr concl)) false hyp0 in
     let dep = dep_in_hyps || dep_in_concl in
     let tmpcl = it_mkNamedProd_or_LetIn concl deps in
     let s = Retyping.get_sort_family_of env sigma tmpcl in
@@ -4207,7 +4216,7 @@ let induction_without_atomization isrec with_evars elim names lid =
 (* assume that no occurrences are selected *)
 let clear_unselected_context id inhyps cls =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
-  if occur_var (Tacmach.New.pf_env gl) id (Tacmach.New.pf_concl gl) &&
+  if occur_var (Tacmach.New.pf_env gl) (Tacmach.New.project gl) id (EConstr.of_constr (Tacmach.New.pf_concl gl)) &&
     cls.concl_occs == NoOccurrences
   then user_err 
     (str "Conclusion must be mentioned: it depends on " ++ pr_id id
@@ -4219,7 +4228,7 @@ let clear_unselected_context id inhyps cls =
 	if Id.List.mem id' inhyps then (* if selected, do not erase *) None
 	else
 	  (* erase if not selected and dependent on id or selected hyps *)
-	  let test id = occur_var_in_decl (Tacmach.New.pf_env gl) id d in
+	  let test id = occur_var_in_decl (Tacmach.New.pf_env gl) (Tacmach.New.project gl) id d in
 	  if List.exists test (id::inhyps) then Some id' else None in
       let ids = List.map_filter to_erase (Proofview.Goal.hyps gl) in
       clear ids
@@ -4246,7 +4255,7 @@ let use_bindings env sigma elim must_be_closed (c,lbind) typ =
   let rec find_clause typ =
     try
       let indclause = make_clenv_binding env sigma (c,typ) lbind in
-      if must_be_closed && occur_meta (clenv_value indclause) then
+      if must_be_closed && occur_meta indclause.evd (EConstr.of_constr (clenv_value indclause)) then
         error "Need a fully applied argument.";
       (* We lose the possibility of coercions in with-bindings *)
       let (sigma, c) = pose_all_metas_as_evars env indclause.evd (clenv_value indclause) in
@@ -4351,10 +4360,10 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
       Sigma (tac, sigma', p +> q)
   end }
 
-let has_generic_occurrences_but_goal cls id env ccl =
+let has_generic_occurrences_but_goal cls id env sigma ccl =
   clause_with_generic_context_selection cls &&
   (* TODO: whd_evar of goal *)
-  (cls.concl_occs != NoOccurrences || not (occur_var env id ccl))
+  (cls.concl_occs != NoOccurrences || not (occur_var env sigma id (EConstr.of_constr ccl)))
 
 let induction_gen clear_flag isrec with_evars elim
     ((_pending,(c,lbind)),(eqname,names) as arg) cls =
@@ -4371,7 +4380,7 @@ let induction_gen clear_flag isrec with_evars elim
     isVar c && not (mem_named_context_val (destVar c) (Global.named_context_val ()))
     && lbind == NoBindings && not with_evars && Option.is_empty eqname
     && clear_flag == None
-    && has_generic_occurrences_but_goal cls (destVar c) env ccl in
+    && has_generic_occurrences_but_goal cls (destVar c) env (Sigma.to_evar_map sigma) ccl in
   let enough_applied = check_enough_applied env sigma elim t in
   if is_arg_pure_hyp && enough_applied then
     (* First case: induction on a variable already in an inductive type and
@@ -4423,11 +4432,12 @@ let induction_gen_l isrec with_evars elim names lc =
 	    | _ ->
                 Proofview.Goal.enter { enter = begin fun gl ->
                 let type_of = Tacmach.New.pf_unsafe_type_of gl in
+                let sigma = Tacmach.New.project gl in
                 let x =
 		  id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
 
                 let id = new_fresh_id [] x gl in
-		let newl' = List.map (replace_term c (mkVar id)) l' in
+		let newl' = List.map (fun r -> replace_term sigma (EConstr.of_constr c) (EConstr.mkVar id) (EConstr.of_constr r)) l' in
 		let _ = newlc:=id::!newlc in
 		Tacticals.New.tclTHEN
 		  (letin_tac None (Name id) c None allHypsAndConcl)
@@ -4601,8 +4611,9 @@ let reflexivity_red allowred =
   (* PL: usual reflexivity don't perform any reduction when searching
      for an equality, but we may need to do some when called back from
      inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
+    let sigma = Tacmach.New.project gl in
     let concl = maybe_betadeltaiota_concl allowred gl in
-    match match_with_equality_type concl with
+    match match_with_equality_type sigma concl with
     | None -> Proofview.tclZERO NoEquationFound
     | Some _ -> one_constructor 1 NoBindings
   end }
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index e4b45489dc..6294f9fdc2 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -351,7 +351,7 @@ struct
       (fun id acc ->
 	 let c_id = Opt.reduce (Ident.constr_of id) in
 	 let (ctx,wc) =
-	   try Termops.align_prod_letin whole_c c_id
+	   try Termops.align_prod_letin Evd.empty (EConstr.of_constr whole_c) (EConstr.of_constr c_id) (** FIXME *)
 	   with Invalid_argument _ -> [],c_id in
 	 let wc,whole_c = if Opt.direction then whole_c,wc else wc,whole_c in
 	 try