Termops API using EConstr.

19 files changed, 100 insertions, 93 deletions

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 2c5b108e5..3ba5da149 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -14,8 +14,8 @@ let get_inductive dir s =
   let glob_ref () = Coqlib.find_reference contrib_name ("Coq" :: dir) s in
   Lazy.from_fun (fun () -> Globnames.destIndRef (glob_ref ()))
 
-let decomp_term (c : Term.constr) =
-  Term.kind_of_term (Termops.strip_outer_cast c)
+let decomp_term sigma (c : Term.constr) =
+  Term.kind_of_term (Termops.strip_outer_cast sigma (EConstr.of_constr c))
 
 let lapp c v  = Term.mkApp (Lazy.force c, v)
 
@@ -105,7 +105,7 @@ module Bool = struct
   | Negb of t
   | Ifb of t * t * t
 
-  let quote (env : Env.t) (c : Term.constr) : t =
+  let quote (env : Env.t) sigma (c : Term.constr) : t =
     let trueb = Lazy.force trueb in
     let falseb = Lazy.force falseb in
     let andb = Lazy.force andb in
@@ -113,7 +113,7 @@ module Bool = struct
     let xorb = Lazy.force xorb in
     let negb = Lazy.force negb in
 
-    let rec aux c = match decomp_term c with
+    let rec aux c = match decomp_term sigma c with
     | Term.App (head, args) ->
       if head === andb && Array.length args = 2 then
         Andb (aux args.(0), aux args.(1))
@@ -181,7 +181,7 @@ module Btauto = struct
     let var = lapp witness [|p|] in
     (* Compute an assignment that dissatisfies the goal *)
     let _, var = Tacmach.pf_reduction_of_red_expr gl (Genredexpr.CbvVm None) var in
-    let rec to_list l = match decomp_term l with
+    let rec to_list l = match decomp_term (Tacmach.project gl) l with
     | Term.App (c, _)
       when c === (Lazy.force CoqList._nil) -> []
     | Term.App (c, [|_; h; t|])
@@ -220,7 +220,7 @@ module Btauto = struct
     Proofview.Goal.nf_enter { enter = begin fun gl ->
       let concl = Proofview.Goal.concl gl in
       let eq = Lazy.force eq in
-      let t = decomp_term concl in
+      let t = decomp_term (Tacmach.New.project gl) concl in
       match t with
       | Term.App (c, [|typ; p; _|]) when c === eq ->
       (* should be an equality [@eq poly ?p (Cst false)] *)
@@ -234,15 +234,16 @@ module Btauto = struct
   let tac =
     Proofview.Goal.nf_enter { enter = begin fun gl ->
       let concl = Proofview.Goal.concl gl in
+      let sigma = Tacmach.New.project gl in
       let eq = Lazy.force eq in
       let bool = Lazy.force Bool.typ in
-      let t = decomp_term concl in
+      let t = decomp_term sigma concl in
       match t with
       | Term.App (c, [|typ; tl; tr|])
           when typ === bool && c === eq ->
           let env = Env.empty () in
-          let fl = Bool.quote env tl in
-          let fr = Bool.quote env tr in
+          let fl = Bool.quote env sigma tl in
+          let fr = Bool.quote env sigma tr in
           let env = Env.to_list env in
           let fl = reify env fl in
           let fr = reify env fr in
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index b5ca2f50f..425bb2d6f 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -58,8 +58,8 @@ let rec decompose_term env sigma t=
 	let tf=decompose_term env sigma f in
 	let targs=Array.map (decompose_term env sigma) args in
 	  Array.fold_left (fun s t->Appli (s,t)) tf targs
-    | Prod (_,a,_b) when not (Termops.dependent (mkRel 1) _b) ->
-	let b = Termops.pop _b in
+    | Prod (_,a,_b) when EConstr.Vars.noccurn sigma 1 (EConstr.of_constr _b) ->
+	let b = Termops.pop (EConstr.of_constr _b) in
 	let sort_b = sf_of env sigma b in
 	let sort_a = sf_of env sigma a in
 	Appli(Appli(Product (sort_a,sort_b) ,
@@ -86,7 +86,7 @@ let rec decompose_term env sigma t=
 	let p' = Projection.map canon_const p in
 	(Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c))
     | _ ->
-       let t = Termops.strip_outer_cast t in
+       let t = Termops.strip_outer_cast sigma (EConstr.of_constr t) in
        if closed0 t then Symb t else raise Not_found
 
 (* decompose equality in members and type *)
@@ -112,8 +112,8 @@ let rec pattern_of_constr env sigma c =
 	  (Array.map_to_list (pattern_of_constr env sigma) args) in
 	  PApp (pf,List.rev pargs),
 	List.fold_left Int.Set.union Int.Set.empty lrels
-    | Prod (_,a,_b) when not (Termops.dependent (mkRel 1) _b) ->
-	let b = Termops.pop _b in
+    | Prod (_,a,_b) when EConstr.Vars.noccurn sigma 1 (EConstr.of_constr _b) ->
+	let b = Termops.pop (EConstr.of_constr _b) in
 	let pa,sa = pattern_of_constr env sigma a in
 	let pb,sb = pattern_of_constr env sigma b in
 	let sort_b = sf_of env sigma b in
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index f68c01b18..65d273faf 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -374,7 +374,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
     match st'.st_it with
 	Thesis nam -> {st_it=Thesis nam;st_label=st'.st_label}
       | This _ -> {st_it = This st.st_it;st_label=st.st_label} in
-  let thyps = fst (match_hyps blend nam2 (Termops.pop rest1) hyps) in
+  let thyps = fst (match_hyps blend nam2 (Termops.pop (EConstr.of_constr rest1)) hyps) in
     tparams,{pat_vars=tpatvars;
 	     pat_aliases=taliases;
 	     pat_constr=pat_pat;
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index e19dc86c4..46fa5b408 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -445,7 +445,7 @@ let concl_refiner metas body gls =
 	    let bsort,_B,nbody =
 	      aux nenv (_x::avoid) ((n,mkVar _x)::subst) rest in
 	    let body = mkNamedLambda _x _A nbody in
-	      if occur_term (mkVar _x) _B then
+	      if local_occur_var evd _x (EConstr.of_constr _B) then
 	        begin
 		  let _P = mkNamedLambda _x _A _B in
 		    match bsort,sort with
@@ -672,14 +672,14 @@ let rec metas_from n hyps =
       _ :: q -> n :: metas_from (succ n) q
     | [] -> []
 
-let rec build_product args body =
+let rec build_product sigma args body =
   match args with
       (Hprop st| Hvar st )::rest ->
-	let pprod= lift 1 (build_product rest body) in
+	let pprod= lift 1 (build_product sigma rest body) in
 	let lbody =
 	  match st.st_label with
 	      Anonymous -> pprod
-	    | Name id -> subst_term (mkVar id) pprod in
+	    | Name id -> subst_var id pprod in
 	  mkProd (st.st_label, st.st_it, lbody)
     | [] -> body
 
@@ -694,7 +694,7 @@ let instr_suffices _then cut gls0 =
   let info = get_its_info gls0 in
   let c_id = pf_get_new_id (Id.of_string "_cofact") gls0 in
   let ctx,hd = cut.cut_stat in
-  let c_stat = build_product ctx (mk_stat_or_thesis info gls0 hd) in
+  let c_stat = build_product (project gls0) ctx (mk_stat_or_thesis info gls0 hd) in
   let metas = metas_from 1 ctx in
   let c_ctx,c_head = build_applist c_stat metas in
   let c_term = applist (mkVar c_id,List.map mkMeta metas) in
@@ -780,7 +780,7 @@ let rec consider_match may_intro introduced available expected gls =
 	  gls
 
 let consider_tac c hyps gls =
-  match kind_of_term (strip_outer_cast c) with
+  match kind_of_term (strip_outer_cast (project gls) (EConstr.of_constr c)) with
       Var id ->
 	consider_match false [] [id] hyps gls
     | _ ->
@@ -805,18 +805,18 @@ let rec take_tac wits gls =
 
 (* tactics for define *)
 
-let rec build_function args body =
+let rec build_function sigma args body =
   match args with
       st::rest ->
-	let pfun= lift 1 (build_function rest body) in
+	let pfun= lift 1 (build_function sigma rest body) in
 	let id = match st.st_label with
 	    Anonymous -> assert false
 	  | Name id -> id in
-	  mkLambda (Name id, st.st_it, subst_term (mkVar id) pfun)
+	  mkLambda (Name id, st.st_it, subst_term sigma (EConstr.mkVar id) (EConstr.of_constr pfun))
     | [] -> body
 
 let define_tac id args body gls =
-  let t = build_function args body in
+  let t = build_function (project gls) args body in
     Proofview.V82.of_tactic (letin_tac None (Name id) t None Locusops.nowhere) gls
 
 (* tactics for reconsider *)
@@ -880,7 +880,7 @@ let build_per_info etype casee gls =
   let concl=pf_concl gls in
   let env=pf_env gls in
   let ctyp=pf_unsafe_type_of gls casee in
-  let is_dep = dependent casee concl in
+  let is_dep = dependent (project gls) (EConstr.of_constr casee) (EConstr.of_constr concl) in
   let hd,args = decompose_app (special_whd gls ctyp) in
   let (ind,u) =
     try
@@ -895,9 +895,9 @@ let build_per_info etype casee gls =
   let params,real_args = List.chop nparams args in
   let abstract_obj c body =
     let typ=pf_unsafe_type_of gls c in
-      lambda_create env (typ,subst_term c body) in
+      lambda_create env (typ,subst_term (project gls) (EConstr.of_constr c) (EConstr.of_constr body)) in
   let pred= List.fold_right abstract_obj
-    real_args (lambda_create env (ctyp,subst_term casee concl)) in
+    real_args (lambda_create env (ctyp,subst_term (project gls) (EConstr.of_constr casee) (EConstr.of_constr concl))) in
     is_dep,
   {per_casee=casee;
    per_ctype=ctyp;
@@ -953,7 +953,7 @@ let suppose_tac hyps gls0 =
   let info = get_its_info gls0 in
   let thesis = pf_concl gls0 in
   let id = pf_get_new_id (Id.of_string "subcase_") gls0 in
-  let clause = build_product hyps thesis in
+  let clause = build_product (project gls0) hyps thesis in
   let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in
   let old_clauses,stack = register_nodep_subcase id info.pm_stack in
   let ninfo2 = {pm_stack=stack} in
@@ -1263,9 +1263,9 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	let params,real_args = List.chop nparams all_args in
 	let abstract_obj c body =
 	  let typ=pf_unsafe_type_of gls c in
-	    lambda_create env (typ,subst_term c body) in
+	    lambda_create env (typ,subst_term (project gls) (EConstr.of_constr c) (EConstr.of_constr body)) in
 	let elim_pred = List.fold_right abstract_obj
-	  real_args (lambda_create env (ctyp,subst_term casee concl)) in
+	  real_args (lambda_create env (ctyp,subst_term (project gls) (EConstr.of_constr casee) (EConstr.of_constr concl))) in
 	let case_info = Inductiveops.make_case_info env ind RegularStyle in
 	let gen_arities = Inductive.arities_of_constructors (ind,u) spec in
 	let f_ids typ =
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index a980a43f5..85cacecdb 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -42,11 +42,11 @@ let none = Evd.empty
 
 let type_of env c =
   let polyprop = (lang() == Haskell) in
-  Retyping.get_type_of ~polyprop env none (strip_outer_cast c)
+  Retyping.get_type_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c))
 
 let sort_of env c =
   let polyprop = (lang() == Haskell) in
-  Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast c)
+  Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c))
 
 (*S Generation of flags and signatures. *)
 
@@ -887,7 +887,7 @@ let extract_std_constant env kn body typ =
      break user's clever let-ins and partial applications). *)
   let rels, c =
     let n = List.length s
-    and m = nb_lam body in
+    and m = nb_lam Evd.empty (EConstr.of_constr body) (** FIXME *) in
     if n <= m then decompose_lam_n n body
     else
       let s,s' = List.chop m s in
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index b34a36492..79f185d18 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -79,13 +79,13 @@ type kind_of_formula=
 let kind_of_formula gl term =
   let normalize=special_nf gl in
   let cciterm=special_whd gl term in
-    match match_with_imp_term cciterm with
-	Some (a,b)-> Arrow(a,(pop b))
+    match match_with_imp_term (project gl) cciterm with
+	Some (a,b)-> Arrow(a,(pop (EConstr.of_constr b)))
       |_->
-	 match match_with_forall_term cciterm with
+	 match match_with_forall_term (project gl) cciterm with
 	     Some (_,a,b)-> Forall(a,b)
 	   |_->
-	      match match_with_nodep_ind cciterm with
+	      match match_with_nodep_ind (project gl) cciterm with
 		  Some (i,l,n)->
 		    let ind,u=destInd i in
 		    let (mib,mip) = Global.lookup_inductive ind in
@@ -96,7 +96,7 @@ let kind_of_formula gl term =
 			let has_realargs=(n>0) in
 			let is_trivial=
 			  let is_constant c =
-			    Int.equal (nb_prod c) mib.mind_nparams in
+			    Int.equal (nb_prod (project gl) (EConstr.of_constr c)) mib.mind_nparams in
 			    Array.exists is_constant mip.mind_nf_lc in
 			  if Inductiveops.mis_is_recursive (ind,mib,mip) ||
 			    (has_realargs && not is_trivial)
@@ -108,7 +108,7 @@ let kind_of_formula gl term =
 			    else
 			      Or((ind,u),l,is_trivial)
 		| _ ->
-		    match match_with_sigma_type cciterm with
+		    match match_with_sigma_type (project gl) cciterm with
 			Some (i,l)-> Exists((destInd i),l)
 		      |_-> Atom (normalize cciterm)
 
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 7ffc78928..1d107e9af 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -38,8 +38,8 @@ let wrap n b continue seq gls=
 	  []->anomaly (Pp.str "Not the expected number of hyps")
 	| nd::q->
             let id = NamedDecl.get_id nd in
-	    if occur_var env id (pf_concl gls) ||
-	      List.exists (occur_var_in_decl env id) ctx then
+	    if occur_var env (project gls) id (EConstr.of_constr (pf_concl gls)) ||
+	      List.exists (occur_var_in_decl env (project gls)  id) ctx then
 		(aux (i-1) q (nd::ctx))
 	    else
 	      add_formula Hyp (VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) gls in
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index d9ab36ad6..01c019744 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -21,7 +21,10 @@ exception UFAIL of constr*constr
    to the equation set. Raises UFAIL with a pair of  terms
 *)
 
+let strip_outer_cast t = strip_outer_cast Evd.empty (EConstr.of_constr t) (** FIXME *)
+
 let unif t1 t2=
+  let evd = Evd.empty in (** FIXME *)
   let bige=Queue.create ()
   and sigma=ref [] in
   let bind i t=
@@ -47,18 +50,18 @@ let unif t1 t2=
 		else bind i nt2
 	  | Meta i,_ ->
 	      let t=subst_meta !sigma nt2 in
-		if Int.Set.is_empty (free_rels t) &&
-		  not (occur_term (mkMeta i) t) then
+		if Int.Set.is_empty (free_rels evd (EConstr.of_constr t)) &&
+		  not (occur_term evd (EConstr.mkMeta i) (EConstr.of_constr t)) then
 		    bind i t else raise (UFAIL(nt1,nt2))
 	  | _,Meta i ->
 	      let t=subst_meta !sigma nt1 in
-		if Int.Set.is_empty (free_rels t) &&
-		  not (occur_term (mkMeta i) t) then
+		if Int.Set.is_empty (free_rels evd (EConstr.of_constr t)) &&
+		  not (occur_term evd (EConstr.mkMeta i) (EConstr.of_constr t)) then
 		    bind i t else raise (UFAIL(nt1,nt2))
 	  | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige
  	  | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast nt2) bige
 	  | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))->
-	      Queue.add (a,c) bige;Queue.add (pop b,pop d) bige
+	      Queue.add (a,c) bige;Queue.add (pop (EConstr.of_constr b),pop (EConstr.of_constr d)) bige
 	  | Case (_,pa,ca,va),Case (_,pb,cb,vb)->
 	      Queue.add (pa,pb) bige;
 	      Queue.add (ca,cb) bige;
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 8e193c753..a14ec8a2c 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -461,8 +461,9 @@ exception GoalDone
 let rec fourier () =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
+    let sigma = Tacmach.New.project gl in
     Coqlib.check_required_library ["Coq";"fourier";"Fourier"];
-    let goal = Termops.strip_outer_cast concl in
+    let goal = Termops.strip_outer_cast sigma (EConstr.of_constr concl) in
     let fhyp=Id.of_string "new_hyp_for_fourier" in
     (* si le but est une inéquation, on introduit son contraire,
        et le but à prouver devient False *)
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 527f4f0b1..f6567ab81 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -287,7 +287,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type  =
     in
     let sub = compute_substitution Int.Map.empty (snd t1) (snd t2) in
     let sub = compute_substitution sub (fst t1) (fst t2) in
-    let end_of_type_with_pop = Termops.pop end_of_type in (*the equation will be removed *)
+    let end_of_type_with_pop = Termops.pop (EConstr.of_constr end_of_type) in (*the equation will be removed *)
     let new_end_of_type =
       (* Ugly hack to prevent Map.fold order change between ocaml-3.08.3 and ocaml-3.08.4
 	 Can be safely replaced by the next comment for Ocaml >= 3.08.4
@@ -309,7 +309,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type  =
 	   try
 	     let witness = Int.Map.find i sub in
 	     if is_local_def decl then anomaly (Pp.str "can not redefine a rel!");
-	     (Termops.pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_name decl, witness, RelDecl.get_type decl, witness_fun))
+	     (Termops.pop (EConstr.of_constr end_of_type),ctxt_size,mkLetIn (RelDecl.get_name decl, witness, RelDecl.get_type decl, witness_fun))
 	   with Not_found  ->
 	     (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun)
 	)
@@ -430,7 +430,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 	  begin
 	    let pte,pte_args =  (destApp t_x) in
 	    let (* fix_info *) prove_rec_hyp = (Id.Map.find (destVar pte) ptes_infos).proving_tac in
-	    let popped_t' = Termops.pop t' in
+	    let popped_t' = Termops.pop (EConstr.of_constr t') in
 	    let real_type_of_hyp = it_mkProd_or_LetIn popped_t' context in
 	    let prove_new_type_of_hyp =
 	      let context_length = List.length context in
@@ -480,7 +480,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 (* 	    observe (str "In "++Ppconstr.pr_id hyp_id++  *)
 (* 		       str " removing useless precond True" *)
 (* 		    );  *)
-	  let popped_t' = Termops.pop t' in
+	  let popped_t' = Termops.pop (EConstr.of_constr t') in
 	  let real_type_of_hyp =
 	    it_mkProd_or_LetIn popped_t' context
 	  in
@@ -508,7 +508,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 	  ]
 	else if is_trivial_eq t_x
 	then (*  t_x :=  t = t   => we remove this precond *)
-	  let popped_t' = Termops.pop t' in
+	  let popped_t' = Termops.pop (EConstr.of_constr t') in
 	  let real_type_of_hyp =
 	    it_mkProd_or_LetIn popped_t' context
 	  in
@@ -608,7 +608,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 	 let fun_body =
 	   mkLambda(Anonymous,
 		    pf_unsafe_type_of g' term,
-		    Termops.replace_term term (mkRel 1) dyn_infos.info
+		    Termops.replace_term (project g') (EConstr.of_constr term) (EConstr.mkRel 1) (EConstr.of_constr dyn_infos.info)
 		   )
 	 in
 	 let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in
@@ -699,7 +699,7 @@ let build_proof
 		  let t = dyn_info'.info in
 		  let dyn_infos = {dyn_info' with info =
 		      mkCase(ci,ct,t,cb)} in
-		  let g_nb_prod = nb_prod (pf_concl g) in
+		  let g_nb_prod = nb_prod (project g) (EConstr.of_constr (pf_concl g)) in
 		  let type_of_term = pf_unsafe_type_of g t in
 		  let term_eq =
 		    make_refl_eq (Lazy.force refl_equal) type_of_term t
@@ -712,7 +712,7 @@ let build_proof
 		      (fun g -> observe_tac "toto" (
 			 tclTHENSEQ [Proofview.V82.of_tactic (Simple.case t);
 				     (fun g' ->
-					let g'_nb_prod = nb_prod (pf_concl g') in
+					let g'_nb_prod = nb_prod (project g') (EConstr.of_constr (pf_concl g')) in
 					let nb_instanciate_partial = g'_nb_prod - g_nb_prod in
 			 		observe_tac "treat_new_case"
 					  (treat_new_case
@@ -927,8 +927,8 @@ let generalize_non_dep hyp g =
     Environ.fold_named_context_reverse (fun (clear,keep) decl ->
       let hyp = get_id decl in
       if Id.List.mem hyp hyps
-        || List.exists (Termops.occur_var_in_decl env hyp) keep
-	|| Termops.occur_var env hyp hyp_typ
+        || List.exists (Termops.occur_var_in_decl env (project g) hyp) keep
+	|| Termops.occur_var env (project g) hyp (EConstr.of_constr hyp_typ)
 	|| Termops.is_section_variable hyp (* should be dangerous *)
       then (clear,decl::keep)
       else (hyp::clear,keep))
@@ -1042,7 +1042,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
       let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd res in 
       res
   in
-  let nb_intro_to_do = nb_prod (pf_concl g) in
+  let nb_intro_to_do = nb_prod (project g) (EConstr.of_constr (pf_concl g)) in
     tclTHEN
       (tclDO nb_intro_to_do (Proofview.V82.of_tactic intro))
       (
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index cc699e5d3..032d887de 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -110,7 +110,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   in
   let dummy_var = mkVar (Id.of_string "________") in
   let mk_replacement c i args =
-    let res = mkApp(rel_to_fun.(i), Array.map Termops.pop (array_get_start args)) in
+    let res = mkApp(rel_to_fun.(i), Array.map (fun c -> Termops.pop (EConstr.of_constr c)) (array_get_start args)) in
     observe (str "replacing " ++ pr_lconstr c ++ str " by "  ++ pr_lconstr res);
     res
   in
@@ -168,25 +168,25 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	let new_env = Environ.push_rel (LocalAssum (x,t)) env in
 	let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
 	 if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
-	 then (Termops.pop new_b), filter_map (eq_constr (mkRel 1)) Termops.pop binders_to_remove_from_b
+	 then (Termops.pop (EConstr.of_constr new_b)), filter_map (eq_constr (mkRel 1)) (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b
 	 else
 	   (
 	     bind_fun(new_x,new_t,new_b),
 	     list_union_eq
 	       eq_constr
 	       binders_to_remove_from_t
-	       (List.map Termops.pop binders_to_remove_from_b)
+	       (List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b)
 	   )
 
        with
 	 | Toberemoved ->
 (* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
 	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b)  in
-	    new_b, List.map Termops.pop binders_to_remove_from_b
+	    new_b, List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b
 	| Toberemoved_with_rel (n,c) ->
 (* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
 	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b)  in
-	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map Termops.pop binders_to_remove_from_b)
+	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b)
     end
   and compute_new_princ_type_for_letin remove env x v t b =
     begin
@@ -197,25 +197,25 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	let new_env = Environ.push_rel (LocalDef (x,v,t)) env in
 	let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
 	if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
-	then (Termops.pop new_b),filter_map (eq_constr (mkRel 1)) Termops.pop binders_to_remove_from_b
+	then (Termops.pop (EConstr.of_constr new_b)),filter_map (eq_constr (mkRel 1)) (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b
 	else
 	  (
 	    mkLetIn(new_x,new_v,new_t,new_b),
 	    list_union_eq
 	      eq_constr
 	      (list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v)
-	      (List.map Termops.pop binders_to_remove_from_b)
+	      (List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b)
 	  )
 
       with
 	| Toberemoved ->
 (* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
 	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b)  in
-	    new_b, List.map Termops.pop binders_to_remove_from_b
+	    new_b, List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b
 	| Toberemoved_with_rel (n,c) ->
 (* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
 	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b)  in
-	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map Termops.pop binders_to_remove_from_b)
+	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b)
     end
   and  compute_new_princ_type_with_acc remove env e (c_acc,to_remove_acc)  =
     let new_e,to_remove_from_e = compute_new_princ_type remove env e
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 99b04898b..a264c37c5 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -14,20 +14,21 @@ open Sigma.Notations
 
 module RelDecl = Context.Rel.Declaration
 
-let is_rec_info scheme_info =
+let is_rec_info sigma scheme_info =
   let test_branche min acc decl =
     acc || (
       let new_branche =
 	it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum (RelDecl.get_type decl))) in
-      let free_rels_in_br = Termops.free_rels new_branche in
+      let free_rels_in_br = Termops.free_rels sigma (EConstr.of_constr new_branche) in
       let max = min + scheme_info.Tactics.npredicates in
       Int.Set.exists (fun i -> i >= min && i< max) free_rels_in_br
     )
   in
   List.fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches)
 
-let choose_dest_or_ind scheme_info =
-  Tactics.induction_destruct (is_rec_info scheme_info) false
+let choose_dest_or_ind scheme_info args =
+  Proofview.tclBIND Proofview.tclEVARMAP (fun sigma ->
+  Tactics.induction_destruct (is_rec_info sigma scheme_info) false args)
 
 let functional_induction with_clean c princl pat =
   let res =
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index c8b4e4833..cf42a809d 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -254,7 +254,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
     let princ_type =  nf_zeta princ_type in
     let princ_infos = Tactics.compute_elim_sig princ_type in
     (* The number of args of the function is then easily computable *)
-    let nb_fun_args = nb_prod (pf_concl g)  - 2  in
+    let nb_fun_args = nb_prod (project g) (EConstr.of_constr (pf_concl g)) - 2 in
     let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in
     let ids = args_names@(pf_ids_of_hyps g) in
     (* Since we cannot ensure that the functional principle is defined in the
@@ -467,7 +467,7 @@ let generalize_dependent_of x hyp g =
   tclMAP
     (function
        | LocalAssum (id,t) when not (Id.equal id hyp) &&
-	   (Termops.occur_var (pf_env g) x t) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id])
+	   (Termops.occur_var (pf_env g) (project g) x (EConstr.of_constr t)) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id])
        | _ -> tclIDTAC
     )
     (pf_hyps g)
@@ -666,7 +666,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     (* Then we get the number of argument of the function
        and compute a fresh name for each of them
     *)
-    let nb_fun_args = nb_prod (pf_concl g)  - 2  in
+    let nb_fun_args = nb_prod (project g) (EConstr.of_constr (pf_concl g)) - 2 in
     let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in
     let ids = args_names@(pf_ids_of_hyps g) in
     (* and fresh names for res H and the principle (cf bug bug #1174) *)
@@ -684,7 +684,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	(fun decl ->
 	   List.map
 	     (fun id -> id)
-	     (generate_fresh_id (Id.of_string "y") ids (nb_prod (RelDecl.get_type decl)))
+	     (generate_fresh_id (Id.of_string "y") ids (nb_prod (project g) (EConstr.of_constr (RelDecl.get_type decl))))
 	)
 	branches
     in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 19c2ed417..865042afb 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -32,7 +32,7 @@ module RelDecl = Context.Rel.Declaration
 
 (** {2 Useful operations on constr and glob_constr} *)
 
-let rec popn i c = if i<=0 then c else pop (popn (i-1) c)
+let rec popn i c = if i<=0 then c else pop (EConstr.of_constr (popn (i-1) c))
 
 (** Substitutions in constr *)
 let compare_constr_nosub t1 t2 =
@@ -985,7 +985,7 @@ let relprinctype_to_funprinctype relprinctype nfuns =
   (* first remove indarg and indarg_in_concl *)
   let relinfo_noindarg = { relinfo with
     indarg_in_concl = false; indarg = None;
-    concl = remove_last_arg (pop relinfo.concl); } in
+    concl = remove_last_arg (pop (EConstr.of_constr relinfo.concl)); } in
   (* the nfuns last induction arguments are functional ones: remove them *)
   let relinfo_argsok = { relinfo_noindarg with
     nargs = relinfo_noindarg.nargs - nfuns;
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 54066edfb..6b63d7771 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -407,7 +407,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
 		let _,args = try destApp ty_teq with DestKO -> assert false in
 		args.(1),args.(2)
 	      in
-	      let new_b' = Termops.replace_term teq_lhs teq_rhs new_b in 
+	      let new_b' = Termops.replace_term (project g') (EConstr.of_constr teq_lhs) (EConstr.of_constr teq_rhs) (EConstr.of_constr new_b) in 
 	      let new_infos = {
 		infos with 
 		  info = new_b';
@@ -681,7 +681,7 @@ let mkDestructEq :
       (fun decl ->
         let open Context.Named.Declaration in
         let id = get_id decl in
-        if Id.List.mem id not_on_hyp || not (Termops.occur_term expr (get_type decl))
+        if Id.List.mem id not_on_hyp || not (Termops.occur_term (project g) (EConstr.of_constr expr) (EConstr.of_constr (get_type decl)))
         then None else Some id) hyps in
   let to_revert_constr = List.rev_map mkVar to_revert in
   let type_of_expr = pf_unsafe_type_of g expr in
@@ -1251,7 +1251,7 @@ let clear_goals =
       | Prod(Name id as na,t',b) ->
 	  let b' = clear_goal b in
 	  if noccurn 1 b' && (is_rec_res id)
-	  then Termops.pop b'
+	  then Termops.pop (EConstr.of_constr b')
 	  else if b' == b then t
 	  else mkProd(na,t',b')
       | _ -> Term.map_constr clear_goal t
@@ -1285,7 +1285,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
           anomaly (Pp.str "open_new_goal with an unamed theorem")
   in
   let na = next_global_ident_away name [] in
-  if Termops.occur_existential gls_type then
+  if Termops.occur_existential sigma (EConstr.of_constr gls_type) then
     CErrors.error "\"abstract\" cannot handle existentials";
   let hook _ _ =
     let opacity =
@@ -1422,7 +1422,7 @@ let start_equation (f:global_reference) (term_f:global_reference)
   (cont_tactic:Id.t list -> tactic) g =
   let ids = pf_ids_of_hyps g in
   let terminate_constr = constr_of_global term_f in
-  let nargs = nb_prod (fst (type_of_const terminate_constr)) (*FIXME*) in
+  let nargs = nb_prod (project g) (EConstr.of_constr (fst (type_of_const terminate_constr))) (*FIXME*) in
   let x = n_x_id ids nargs in
   observe_tac (str "start_equation") (observe_tclTHENLIST (str "start_equation") [
     h_intros x;
@@ -1552,7 +1552,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       and functional_ref = destConst (constr_of_global functional_ref)
       and eq_ref = destConst (constr_of_global eq_ref) in
       generate_induction_principle f_ref tcc_lemma_constr
-	functional_ref eq_ref rec_arg_num rec_arg_type (nb_prod res) relation;
+	functional_ref eq_ref rec_arg_num rec_arg_type (nb_prod evm (EConstr.of_constr res)) relation;
       if Flags.is_verbose ()
       then msgnl (h 1 (Ppconstr.pr_id function_name ++
 			 spc () ++ str"is defined" )++ fnl () ++
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index a063cbbfe..49fcf83b4 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1221,7 +1221,7 @@ struct
           let g,env,tg = xparse_formula env tg b in
           mkformula_binary mkIff term f g,env,tg
         | _ -> parse_atom env tg term)
-      | Prod(typ,a,b) when not (Termops.dependent (mkRel 1) b)->
+      | Prod(typ,a,b) when EConstr.Vars.noccurn Evd.empty 1 (EConstr.of_constr b) (** FIXME *) ->
         let f,env,tg = xparse_formula env tg a in
         let g,env,tg = xparse_formula env tg b in
         mkformula_binary mkI term f g,env,tg
@@ -1687,7 +1687,8 @@ let rec mk_topo_order le l =
   | (Some v,l') -> v ::  (mk_topo_order le l')
 
     
-let topo_sort_constr l = mk_topo_order Termops.dependent l
+let topo_sort_constr l =
+  mk_topo_order (fun c t -> Termops.dependent Evd.empty (** FIXME *) (EConstr.of_constr c) (EConstr.of_constr t)) l
 
 
 (**
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 6405c8ceb..c6376727a 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -183,7 +183,7 @@ type inversion_scheme = {
 
 let i_can't_do_that () = error "Quote: not a simple fixpoint"
 
-let decomp_term c = kind_of_term (Termops.strip_outer_cast c)
+let decomp_term gl c = kind_of_term (Termops.strip_outer_cast (Tacmach.New.project gl) (EConstr.of_constr c))
 
 (*s [compute_lhs typ i nargsi] builds the term \texttt{(C ?nargsi ...
   ?2 ?1)}, where \texttt{C} is the [i]-th constructor of inductive
@@ -223,14 +223,14 @@ let compute_rhs bodyi index_of_f =
 let compute_ivs f cs gl =
   let cst = try destConst f with DestKO -> i_can't_do_that () in
   let body = Environ.constant_value_in (Global.env()) cst in
-  match decomp_term body with
+  match decomp_term gl body with
     | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) ->
         let (args3, body3) = decompose_lam body2 in
         let nargs3 = List.length args3 in
         let env = Proofview.Goal.env gl in
         let sigma = Tacmach.New.project gl in
         let is_conv = Reductionops.is_conv env sigma in
-          begin match decomp_term body3 with
+          begin match decomp_term gl body3 with
           | Case(_,p,c,lci) -> (* <p> Case c of c1 ... cn end *)
               let n_lhs_rhs = ref []
               and v_lhs = ref (None : constr option)
@@ -267,7 +267,7 @@ let compute_ivs f cs gl =
 
 	      (* The Cases predicate is a lambda; we assume no dependency *)
 	      let p = match kind_of_term p with
-		| Lambda (_,_,p) -> Termops.pop p
+		| Lambda (_,_,p) -> Termops.pop (EConstr.of_constr p)
 		| _ -> p
 	      in
 
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 367a13333..b129b0bb3 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -94,7 +94,7 @@ let rec make_form atom_env gls term =
   let cciterm=special_whd gls term  in
     match kind_of_term cciterm with
 	Prod(_,a,b) ->
-	  if not (Termops.dependent (mkRel 1) b) &&
+	  if EConstr.Vars.noccurn Evd.empty (** FIXME *) 1 (EConstr.of_constr b) &&
 	    Retyping.get_sort_family_of
 	    (pf_env gls) (Tacmach.project gls) a == InProp
 	  then
@@ -134,7 +134,7 @@ let rec make_hyps atom_env gls lenv = function
   | LocalAssum (id,typ)::rest ->
       let hrec=
 	make_hyps atom_env gls (typ::lenv) rest in
-	if List.exists (Termops.dependent (mkVar id)) lenv ||
+	if List.exists (fun c -> Termops.local_occur_var Evd.empty (** FIXME *) id (EConstr.of_constr c)) lenv ||
 	  (Retyping.get_sort_family_of
 	     (pf_env gls) (Tacmach.project gls) typ != InProp)
 	then
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 77e25b2a5..86cc928c8 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -702,7 +702,7 @@ let match_upats_HO ~on_instance upats env sigma0 ise c =
 
 let fixed_upat = function
 | {up_k = KpatFlex | KpatEvar _ | KpatProj _} -> false 
-| {up_t = t} -> not (occur_existential t)
+| {up_t = t} -> not (occur_existential Evd.empty (EConstr.of_constr t)) (** FIXME *)
 
 let do_once r f = match !r with Some _ -> () | None -> r := Some (f ())