Remove some occurrences of "open Termops"

Functions from Termops were sometimes fully qualified, sometimes not
in the same module. This commit makes their usage more uniform.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13470 85f007b7-540e-0410-9357-904b9bb8a0f7

21 files changed, 138 insertions, 159 deletions

diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 64b8b7bc9..6f0896cc8 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -19,7 +19,6 @@ open Pattern
 open Ppextend
 open Ppconstr
 open Printer
-open Termops
 
 let pr_global x = Nametab.pr_global_env Idset.empty x
 
@@ -388,11 +387,11 @@ let pr_by_tactic prt = function
   | tac -> spc() ++ str "by " ++ prt tac
 
 let pr_hyp_location pr_id = function
-  | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs
-  | occs, InHypTypeOnly ->
+  | occs, Termops.InHyp -> spc () ++ pr_with_occurrences pr_id occs
+  | occs, Termops.InHypTypeOnly ->
       spc () ++
       pr_with_occurrences (fun id -> str "(type of " ++ pr_id id ++ str ")") occs
-  | occs, InHypValueOnly ->
+  | occs, Termops.InHypValueOnly ->
       spc () ++
       pr_with_occurrences (fun id -> str "(value of " ++ pr_id id ++ str ")") occs
 
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 34637b1e8..c575fde52 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -11,7 +11,6 @@ open Util
 open Names
 open Nameops
 open Term
-open Termops
 open Sign
 open Environ
 open Global
@@ -62,7 +61,7 @@ let pr_constr_under_binders_env_gen pr env (ids,c) =
   (* we also need to preserve the actual names of the patterns *)
   (* So what to do? *)
   let assums = List.map (fun id -> (Name id,(* dummy *) mkProp)) ids in
-  pr (push_rels_assum assums env) c
+  pr (Termops.push_rels_assum assums env) c
 
 let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_constr_env
 let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_lconstr_env
@@ -88,9 +87,9 @@ let pr_ljudge_env env j =
 let pr_ljudge j = pr_ljudge_env (Global.env()) j
 
 let pr_lrawconstr_env env c =
-  pr_lconstr_expr (extern_rawconstr (vars_of_env env) c)
+  pr_lconstr_expr (extern_rawconstr (Termops.vars_of_env env) c)
 let pr_rawconstr_env env c =
-  pr_constr_expr (extern_rawconstr (vars_of_env env) c)
+  pr_constr_expr (extern_rawconstr (Termops.vars_of_env env) c)
 
 let pr_lrawconstr c =
   pr_lconstr_expr (extern_rawconstr Idset.empty c)
@@ -101,14 +100,14 @@ let pr_cases_pattern t =
   pr_cases_pattern_expr (extern_cases_pattern Idset.empty t)
 
 let pr_lconstr_pattern_env env c =
-  pr_lconstr_pattern_expr (extern_constr_pattern (names_of_rel_context env) c)
+  pr_lconstr_pattern_expr (extern_constr_pattern (Termops.names_of_rel_context env) c)
 let pr_constr_pattern_env env c =
-  pr_constr_pattern_expr (extern_constr_pattern (names_of_rel_context env) c)
+  pr_constr_pattern_expr (extern_constr_pattern (Termops.names_of_rel_context env) c)
 
 let pr_lconstr_pattern t =
-  pr_lconstr_pattern_expr (extern_constr_pattern empty_names_context t)
+  pr_lconstr_pattern_expr (extern_constr_pattern Termops.empty_names_context t)
 let pr_constr_pattern t =
-  pr_constr_pattern_expr (extern_constr_pattern empty_names_context t)
+  pr_constr_pattern_expr (extern_constr_pattern Termops.empty_names_context t)
 
 let pr_sort s = pr_rawsort (extern_sort s)
 
@@ -120,7 +119,7 @@ let _ = Termops.set_print_constr pr_lconstr_env
 let pr_global_env = pr_global_env
 let pr_global = pr_global_env Idset.empty
 
-let pr_constant env cst = pr_global_env (vars_of_env env) (ConstRef cst)
+let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst)
 let pr_existential env ev = pr_lconstr_env env (mkEvar ev)
 let pr_inductive env ind = pr_lconstr_env env (mkInd ind)
 let pr_constructor env cstr = pr_lconstr_env env (mkConstruct cstr)
@@ -438,7 +437,7 @@ let pr_prim_rule = function
         | [] -> mt () in
       (str"cofix " ++ pr_id f ++  str" with " ++ print_mut others)
   | Refine c ->
-      str(if occur_meta c then "refine " else "exact ") ++
+      str(if Termops.occur_meta c then "refine " else "exact ") ++
       Constrextern.with_meta_as_hole pr_constr c
 
   | Convert_concl (c,_) ->
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 1054b6ecd..ec31f8917 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -18,7 +18,6 @@ open Nameops
 open Inductiveops
 open Declarations
 open Term
-open Termops
 open Tacmach
 open Tactics
 open Tacticals
@@ -64,8 +63,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 (dependent (mkRel 1) _b) ->
-	let b = pop _b in
+    | Prod (_,a,_b) when not (Termops.dependent (mkRel 1) _b) ->
+	let b = Termops.pop _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) ,
@@ -111,8 +110,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 Intset.union Intset.empty lrels
-    | Prod (_,a,_b) when not (dependent (mkRel 1) _b) ->
-	let b =pop _b in
+    | Prod (_,a,_b) when not (Termops.dependent (mkRel 1) _b) ->
+	let b = Termops.pop _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
@@ -258,19 +257,19 @@ let rec proof_tac p gls =
     | SymAx c ->
 	let l=constr_of_term p.p_lhs and
 	    r=constr_of_term p.p_rhs in
-        let typ = refresh_universes (pf_type_of gls l) in
+        let typ = Termops.refresh_universes (pf_type_of gls l) in
 	  exact_check
 	    (mkApp(Lazy.force _sym_eq,[|typ;r;l;c|])) gls
     | Refl t ->
 	let lr = constr_of_term t in
-	let typ = refresh_universes (pf_type_of gls lr) in
+	let typ = Termops.refresh_universes (pf_type_of gls lr) in
 	exact_check
 	   (mkApp(Lazy.force _refl_equal,[|typ;constr_of_term t|])) gls
     | Trans (p1,p2)->
 	let t1 = constr_of_term p1.p_lhs and
 	    t2 = constr_of_term p1.p_rhs and
 	    t3 = constr_of_term p2.p_rhs in
-	let typ = refresh_universes (pf_type_of gls t2) in
+	let typ = Termops.refresh_universes (pf_type_of gls t2) in
 	let prf =
 	  mkApp(Lazy.force _trans_eq,[|typ;t1;t2;t3;_M 1;_M 2|]) in
 	  tclTHENS (refine prf) [(proof_tac p1);(proof_tac p2)] gls
@@ -279,9 +278,9 @@ let rec proof_tac p gls =
 	and tx1=constr_of_term p2.p_lhs
 	and tf2=constr_of_term p1.p_rhs
 	and tx2=constr_of_term p2.p_rhs in
-	let typf = refresh_universes (pf_type_of gls tf1) in
-	let typx = refresh_universes (pf_type_of gls tx1) in
-	let typfx = refresh_universes (pf_type_of gls (mkApp (tf1,[|tx1|]))) in
+	let typf = Termops.refresh_universes (pf_type_of gls tf1) in
+	let typx = Termops.refresh_universes (pf_type_of gls tx1) in
+	let typfx = Termops.refresh_universes (pf_type_of gls (mkApp (tf1,[|tx1|]))) in
 	let id = pf_get_new_id (id_of_string "f") gls in
 	let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
 	let lemma1 =
@@ -309,8 +308,8 @@ let rec proof_tac p gls =
 	 let ti=constr_of_term prf.p_lhs in
 	 let tj=constr_of_term prf.p_rhs in
 	 let default=constr_of_term p.p_lhs in
-	 let intype=refresh_universes (pf_type_of gls ti) in
-	 let outtype=refresh_universes (pf_type_of gls default) in
+	 let intype = Termops.refresh_universes (pf_type_of gls ti) in
+	 let outtype = Termops.refresh_universes (pf_type_of gls default) in
 	 let special=mkRel (1+nargs-argind) in
 	 let proj=build_projection intype outtype cstr special default gls in
 	 let injt=
@@ -319,7 +318,7 @@ let rec proof_tac p gls =
 
 let refute_tac c t1 t2 p gls =
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
-  let intype=refresh_universes (pf_type_of gls tt1) in
+  let intype = Termops.refresh_universes (pf_type_of gls tt1) in
   let neweq=
     mkApp(Lazy.force _eq,
 	  [|intype;tt1;tt2|]) in
@@ -330,7 +329,7 @@ let refute_tac c t1 t2 p gls =
 
 let convert_to_goal_tac c t1 t2 p gls =
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
-  let sort=refresh_universes (pf_type_of gls tt2) in
+  let sort = Termops.refresh_universes (pf_type_of gls tt2) in
   let neweq=mkApp(Lazy.force _eq,[|sort;tt1;tt2|]) in
   let e=pf_get_new_id (id_of_string "e") gls in
   let x=pf_get_new_id (id_of_string "X") gls in
@@ -350,14 +349,14 @@ let convert_to_hyp_tac c1 t1 c2 t2 p gls =
 
 let discriminate_tac cstr p gls =
   let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
-  let intype=refresh_universes (pf_type_of gls t1) in
+  let intype = Termops.refresh_universes (pf_type_of gls t1) in
   let concl=pf_concl gls in
-  let outsort=mkType (new_univ ()) in
+  let outsort = mkType (Termops.new_univ ()) in
   let xid=pf_get_new_id (id_of_string "X") gls in
   let tid=pf_get_new_id (id_of_string "t") gls in
   let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in
   let trivial=pf_type_of gls identity in
-  let outtype=mkType (new_univ ()) in
+  let outtype = mkType (Termops.new_univ ()) in
   let pred=mkLambda(Name xid,outtype,mkRel 1) in
   let hid=pf_get_new_id (id_of_string "Heq") gls in
   let proj=build_projection intype outtype cstr trivial concl gls in
@@ -412,7 +411,7 @@ let cc_tactic depth additionnal_terms gls=
 			 str "\"congruence with (" ++
 			 prlist_with_sep
 			   (fun () -> str ")" ++ pr_spc () ++ str "(")
-			   (print_constr_env (pf_env gls))
+			   (Termops.print_constr_env (pf_env gls))
 			   terms_to_complete ++
 			 str ")\","
 		       end);
@@ -454,7 +453,7 @@ let simple_reflexivity () = apply (Lazy.force _refl_equal)
 
 let f_equal gl =
   let cut_eq c1 c2 =
-    let ty = refresh_universes (pf_type_of gl c1) in
+    let ty = Termops.refresh_universes (pf_type_of gl c1) in
     tclTHENTRY
       (Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|])))
       (simple_reflexivity ())
diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml
index b800170de..22ae4aaf9 100644
--- a/plugins/dp/dp.ml
+++ b/plugins/dp/dp.ml
@@ -23,7 +23,6 @@ open Fol
 open Names
 open Nameops
 open Namegen
-open Termops
 open Coqlib
 open Hipattern
 open Libnames
@@ -148,7 +147,7 @@ let fresh_var = function
    env names, and returns the new variables together with the new
    environment *)
 let coq_rename_vars env vars =
-  let avoid = ref (ids_of_named_context (Environ.named_context env)) in
+  let avoid = ref (Termops.ids_of_named_context (Environ.named_context env)) in
   List.fold_right
     (fun (na,t) (newvars, newenv) ->
        let id = next_name_away na !avoid in
@@ -183,7 +182,7 @@ let decomp_type_lambdas env t =
 
 let decompose_arrows =
   let rec arrows_rec l c = match kind_of_term c with
-    | Prod (_,t,c) when not (dependent (mkRel 1) c) -> arrows_rec (t :: l) c
+    | Prod (_,t,c) when not (Termops.dependent (mkRel 1) c) -> arrows_rec (t :: l) c
     | Cast (c,_,_) -> arrows_rec l c
     | _ -> List.rev l, c
   in
@@ -195,8 +194,8 @@ let rec eta_expanse t vars env i =
     t, vars, env
   else
     match kind_of_term (Typing.type_of env Evd.empty t) with
-      | Prod (n, a, b) when not (dependent (mkRel 1) b) ->
-	  let avoid = ids_of_named_context (Environ.named_context env) in
+      | Prod (n, a, b) when not (Termops.dependent (mkRel 1) b) ->
+	  let avoid = Termops.ids_of_named_context (Environ.named_context env) in
 	  let id = next_name_away n avoid in
 	  let env' = Environ.push_named (id, None, a) env in
 	  let t' = mkApp (t, [| mkVar id |]) in
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index bc12fcea9..43658e802 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1,7 +1,6 @@
 open Printer
 open Util
 open Term
-open Termops
 open Namegen
 open Names
 open Declarations
@@ -263,7 +262,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
     in
     let sub = compute_substitution Intmap.empty (snd t1) (snd t2) in
     let sub = compute_substitution sub (fst t1) (fst t2) in
-    let end_of_type_with_pop = pop end_of_type in (*the equation will be removed *)
+    let end_of_type_with_pop = Termops.pop 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
@@ -286,7 +285,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
 	   try
 	     let witness = Intmap.find i sub in
 	     if b' <> None then anomaly "can not redefine a rel!";
-	     (pop end_of_type,ctxt_size,mkLetIn(x',witness,t',witness_fun))
+	     (Termops.pop end_of_type,ctxt_size,mkLetIn(x',witness,t',witness_fun))
 	   with Not_found  ->
 	     (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun)
 	)
@@ -411,7 +410,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 = (Idmap.find (destVar pte) ptes_infos).proving_tac in
-	    let popped_t' = pop t' in
+	    let popped_t' = Termops.pop 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
@@ -461,7 +460,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' = pop t' in
+	  let popped_t' = Termops.pop t' in
 	  let real_type_of_hyp =
 	    it_mkProd_or_LetIn popped_t' context
 	  in
@@ -489,7 +488,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' = pop t' in
+	  let popped_t' = Termops.pop t' in
 	  let real_type_of_hyp =
 	    it_mkProd_or_LetIn popped_t' context
 	  in
@@ -589,7 +588,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 	 let fun_body =
 	   mkLambda(Anonymous,
 		    pf_type_of g' term,
-		    replace_term term (mkRel 1) dyn_infos.info
+		    Termops.replace_term term (mkRel 1) dyn_infos.info
 		   )
 	 in
 	 let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in
@@ -909,8 +908,8 @@ let generalize_non_dep hyp g =
   let to_revert,_ =
     Environ.fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) ->
       if List.mem hyp hyps
-	or List.exists (occur_var_in_decl env hyp) keep
-	or occur_var env hyp hyp_typ
+	or List.exists (Termops.occur_var_in_decl env hyp) keep
+	or Termops.occur_var env hyp hyp_typ
 	or Termops.is_section_variable hyp (* should be dangerous *)
       then (clear,decl::keep)
       else (hyp::clear,keep))
@@ -1300,7 +1299,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		 in
 		 let fname = destConst (fst (decompose_app (List.hd (List.rev pte_args)))) in
 		 tclTHENSEQ
-		   [unfold_in_concl [(all_occurrences,Names.EvalConstRef fname)];
+		   [unfold_in_concl [(Termops.all_occurrences, Names.EvalConstRef fname)];
 		    let do_prove =
 		      build_proof
 			interactive_proof
@@ -1400,7 +1399,7 @@ let build_clause eqs =
   {
     Tacexpr.onhyps =
       Some (List.map
-	      (fun id -> (Rawterm.all_occurrences_expr,id),InHyp)
+	      (fun id -> (Rawterm.all_occurrences_expr, id), Termops.InHyp)
 	      eqs
 	   );
     Tacexpr.concl_occs = Rawterm.no_occurrences_expr
@@ -1416,7 +1415,7 @@ let rec rewrite_eqs_in_eqs eqs =
 	       (fun id gl ->
 		  observe_tac
 		    (Format.sprintf "rewrite %s in %s " (string_of_id eq) (string_of_id id))
-		    (tclTRY (Equality.general_rewrite_in true all_occurrences (* dep proofs also: *) true id (mkVar eq) false))
+		    (tclTRY (Equality.general_rewrite_in true Termops.all_occurrences (* dep proofs also: *) true id (mkVar eq) false))
 		    gl
 	       )
 	       eqs
@@ -1438,7 +1437,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
 		  (fun g ->
 		     if is_mes
 		     then
-		       unfold_in_concl [(all_occurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g
+		       unfold_in_concl [(Termops.all_occurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g
 		     else tclIDTAC g
 		  );
 		  observe_tac "rew_and_finish"
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index e0b08599d..6034f19e6 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -1,7 +1,6 @@
 open Printer
 open Util
 open Term
-open Termops
 open Namegen
 open Names
 open Declarations
@@ -139,7 +138,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 pop (array_get_start args)) in
+    let res = mkApp(rel_to_fun.(i), Array.map Termops.pop (array_get_start args)) in
 (*     observe (str "replacing " ++ pr_lconstr c ++ str " by "  ++ pr_lconstr res); *)
     res
   in
@@ -198,58 +197,58 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
     begin
       try
 	let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in
-	let new_x : name = get_name (ids_of_context env) x in
+	let new_x : name = get_name (Termops.ids_of_context env) x in
 	let new_env = Environ.push_rel (x,None,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 (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
+	 then (Termops.pop new_b), filter_map (eq_constr (mkRel 1)) Termops.pop 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 pop binders_to_remove_from_b)
+	       (List.map Termops.pop 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 pop binders_to_remove_from_b
+	    new_b, List.map Termops.pop 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 pop binders_to_remove_from_b)
+	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map Termops.pop binders_to_remove_from_b)
     end
   and compute_new_princ_type_for_letin remove env x v t b =
     begin
       try
 	let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in
 	let new_v,binders_to_remove_from_v = compute_new_princ_type remove env v in
-	let new_x : name = get_name (ids_of_context env) x in
+	let new_x : name = get_name (Termops.ids_of_context env) x in
 	let new_env = Environ.push_rel (x,Some 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 (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
+	then (Termops.pop new_b),filter_map (eq_constr (mkRel 1)) Termops.pop 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 pop binders_to_remove_from_b)
+	      (List.map Termops.pop 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 pop binders_to_remove_from_b
+	    new_b, List.map Termops.pop 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 pop binders_to_remove_from_b)
+	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map Termops.pop 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/invfun.ml b/plugins/funind/invfun.ml
index f0ea133c6..24382f875 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -16,7 +16,6 @@ open Tacticals
 open Tactics
 open Indfun_common
 open Tacmach
-open Termops
 open Sign
 open Hiddentac
 
@@ -686,7 +685,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	  h_generalize (List.map mkVar ids);
 	  thin ids
 	]
-      else unfold_in_concl [(all_occurrences,Names.EvalConstRef (destConst f))]
+      else unfold_in_concl [(Termops.all_occurrences, Names.EvalConstRef (destConst f))]
     in
     (* The proof of each branche itself *)
     let ind_number = ref 0 in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index e329196ac..c42ecac42 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -9,7 +9,6 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
 open Term
-open Termops
 open Namegen
 open Environ
 open Declarations
@@ -374,7 +373,7 @@ let rec  mk_intros_and_continue thin_intros (extra_eqn:bool)
 		h_intros thin_intros;
 
 		tclMAP
-		  (fun eq -> tclTRY (Equality.general_rewrite_in true all_occurrences (* deps proofs also: *) true teq eq false))
+		  (fun eq -> tclTRY (Equality.general_rewrite_in true Termops.all_occurrences (* deps proofs also: *) true teq eq false))
 		  (List.rev eqs);
 		(fun g1 ->
 		   let ty_teq = pf_type_of g1 (mkVar teq) in
@@ -382,7 +381,7 @@ let rec  mk_intros_and_continue thin_intros (extra_eqn:bool)
 		     let _,args = try destApp ty_teq with _ -> Pp.msgnl (Printer.pr_goal g1 ++ fnl () ++ pr_id teq ++ str ":" ++ Printer.pr_lconstr ty_teq); assert false in
 		     args.(1),args.(2)
 		   in
-	           cont_function (mkVar teq::eqs) (replace_term teq_lhs teq_rhs expr) g1
+	           cont_function (mkVar teq::eqs) (Termops.replace_term teq_lhs teq_rhs expr) g1
 		)
 	      ]
 	      
@@ -435,7 +434,7 @@ let tclUSER tac is_mes l g =
       clear_tac;
       if is_mes
       then tclTHEN
-             (unfold_in_concl [(all_occurrences, evaluable_of_global_reference
+             (unfold_in_concl [(Termops.all_occurrences, evaluable_of_global_reference
                                       (delayed_force ltof_ref))])
              tac
       else tac
@@ -534,7 +533,7 @@ let rec list_cond_rewrite k def pmax cond_eqs le_proofs =
 	   Nameops.out_name k_na,Nameops.out_name def_na
 	 in
 	 tclTHENS
-	   (general_rewrite_bindings false all_occurrences
+	   (general_rewrite_bindings false Termops.all_occurrences
 	      (* dep proofs also: *) true
 	      (mkVar eq,
 	       ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k;
@@ -577,7 +576,7 @@ let rec introduce_all_equalities func eqs values specs bound le_proofs
 	   observe_tac "refl equal" (apply (delayed_force refl_equal))] g
   | spec1::specs ->
       fun g ->
-	let ids = ids_of_named_context (pf_hyps g) in
+	let ids = Termops.ids_of_named_context (pf_hyps g) in
 	let p = next_ident_away_in_goal p_id ids in
         let ids = p::ids in
 	let pmax = next_ident_away_in_goal pmax_id ids in
@@ -623,7 +622,7 @@ let rec introduce_all_values concl_tac is_mes acc_inv func context_fn
 	   (List.rev values) (List.rev specs) (delayed_force coq_O) [] [])]
   | arg::args ->
       (fun g ->
-	let ids = ids_of_named_context (pf_hyps g) in
+	let ids = Termops.ids_of_named_context (pf_hyps g) in
 	let rec_res = next_ident_away_in_goal rec_res_id ids in
         let ids = rec_res::ids in
 	let hspec = next_ident_away_in_goal hspec_id ids in
@@ -836,7 +835,7 @@ let rec instantiate_lambda t l =
 let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_arg_num  : tactic =
   begin
     fun g ->
-      let ids = ids_of_named_context (pf_hyps g) in
+      let ids = Termops.ids_of_named_context (pf_hyps g) in
       let func_body = (def_of_const (constr_of_global func)) in
       let (f_name, _, body1) = destLambda func_body in
       let f_id =
@@ -924,7 +923,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 pop b'
+	  then Termops.pop b'
 	  else if b' == b then t
 	  else mkProd(na,t',b')
       | _ -> map_constr clear_goal t
@@ -952,7 +951,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
   let sign = Global.named_context () in
   let sign = clear_proofs sign in
   let na = next_global_ident_away name [] in
-  if occur_existential gls_type then
+  if Termops.occur_existential gls_type then
     Util.error "\"abstract\" cannot handle existentials";
   let hook _ _ =
     let opacity =
@@ -1158,7 +1157,7 @@ let start_equation (f:global_reference) (term_f:global_reference)
   let x = n_x_id ids nargs in
   tclTHENLIST [
     h_intros x;
-    unfold_in_concl [(all_occurrences, evaluable_of_global_reference f)];
+    unfold_in_concl [(Termops.all_occurrences, evaluable_of_global_reference f)];
     observe_tac "simplest_case"
       (simplest_case (mkApp (terminate_constr,
                              Array.of_list (List.map mkVar x))));
@@ -1200,7 +1199,7 @@ let rec introduce_all_values_eq cont_tac functional termine
            simpl_iter (onHyp heq2);
            unfold_in_hyp [((true,[1]), evaluable_of_global_reference
                              (global_of_constr functional))]
-             (heq2, InHyp);
+             (heq2, Termops.InHyp);
            tclTHENS
 	     (fun gls ->
 		let t_eq = compute_renamed_type gls (mkVar heq2) in
@@ -1208,7 +1207,7 @@ let rec introduce_all_values_eq cont_tac functional termine
 		  let _,_,t  = destProd t_eq in let def_na,_,_ = destProd t in
 		  Nameops.out_name def_na
 		in
-		observe_tac "rewrite heq" (general_rewrite_bindings false all_occurrences
+		observe_tac "rewrite heq" (general_rewrite_bindings false Termops.all_occurrences
 		(* dep proofs also: *) true (mkVar heq2,
 		 ExplicitBindings[dummy_loc,NamedHyp def_id,
 				  f]) false) gls)
@@ -1264,7 +1263,7 @@ let rec introduce_all_values_eq cont_tac functional termine
 			       f_S(mkVar pmax');
 			       dummy_loc, NamedHyp def_id, f])
 			 in
-			   observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false all_occurrences (* dep proofs also: *) true
+			   observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false Termops.all_occurrences (* dep proofs also: *) true
 							       c_b false))
 			     g
 		     )
@@ -1321,7 +1320,7 @@ let rec prove_eq nb_arg  (termine:constr) (f:constr)(functional:global_reference
 		_,[] -> observe_tac "base_leaf_eq(1)" (base_leaf_eq functional eqs f)
 	      | fn,args ->
 	        fun g ->
-		  let ids = ids_of_named_context (pf_hyps g) in
+		  let ids = Termops.ids_of_named_context (pf_hyps g) in
 	          observe_tac "rec_leaf_eq" (rec_leaf_eq termine f ids
 		    (constr_of_global functional)
 		    eqs expr fn args) g))
@@ -1330,7 +1329,7 @@ let rec prove_eq nb_arg  (termine:constr) (f:constr)(functional:global_reference
 		_,[] -> observe_tac "base_leaf_eq(2)" ( base_leaf_eq functional eqs f)
 	      | fn,args ->
 		  fun g ->
-		    let ids = ids_of_named_context (pf_hyps g) in
+		    let ids = Termops.ids_of_named_context (pf_hyps g) in
 		    observe_tac "rec_leaf_eq" (rec_leaf_eq
 		      termine f ids (constr_of_global functional)
 		      eqs expr fn args) g));;
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index c457115d3..c36cded17 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -20,7 +20,6 @@ open Proof_type
 open Names
 open Nameops
 open Term
-open Termops
 open Declarations
 open Environ
 open Sign
@@ -131,7 +130,7 @@ let exists_tac c = constructor_tac false (Some 1) 1 (Rawterm.ImplicitBindings [c
 let generalize_tac t = generalize_time (generalize t)
 let elim t = elim_time (simplest_elim t)
 let exact t = exact_time (Tactics.refine t)
-let unfold s = Tactics.unfold_in_concl [all_occurrences, Lazy.force s]
+let unfold s = Tactics.unfold_in_concl [Termops.all_occurrences, Lazy.force s]
 
 let rev_assoc k =
   let rec loop = function
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 3e9cc781f..cd4a7d3b0 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -10,7 +10,6 @@ module Search = Explore.Make(Proof_search)
 
 open Util
 open Term
-open Termops
 open Names
 open Evd
 open Tacmach
@@ -102,7 +101,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 (dependent (mkRel 1) b) &&
+	  if not (Termops.dependent (mkRel 1) b) &&
 	    Retyping.get_sort_family_of
 	    (pf_env gls) (Tacmach.project gls) a = InProp
 	  then
@@ -142,7 +141,7 @@ let rec make_hyps atom_env gls lenv = function
   | (id,None,typ)::rest ->
       let hrec=
 	make_hyps atom_env gls (typ::lenv) rest in
-	if List.exists (dependent (mkVar id)) lenv ||
+	if List.exists (Termops.dependent (mkVar id)) lenv ||
 	  (Retyping.get_sort_family_of
 	     (pf_env gls) (Tacmach.project gls) typ <> InProp)
 	then
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 052406867..741d22a8a 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -17,7 +17,6 @@ open Environ
 open Libnames
 open Tactics
 open Rawterm
-open Termops
 open Tacticals
 open Tacexpr
 open Pcoq
@@ -102,7 +101,7 @@ let protect_tac map =
   Tactics.reduct_option (protect_red map,DEFAULTcast) None ;;
 
 let protect_tac_in map id =
-  Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id,InHyp));;
+  Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Termops.InHyp));;
 
 
 TACTIC EXTEND protect_fv
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 93f9b586b..31e630741 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -20,7 +20,6 @@ open Constrintern
 open Subtac_command
 open Typeclasses
 open Typeclasses_errors
-open Termops
 open Decl_kinds
 open Entries
 open Util
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 634a6ea60..397bda9b0 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -21,7 +21,6 @@ open Tacmach
 open Tactic_debug
 open Topconstr
 open Term
-open Termops
 open Tacexpr
 open Safe_typing
 open Typing
@@ -133,7 +132,7 @@ let collect_non_rec env =
       let i =
         list_try_find_i
           (fun i f ->
-             if List.for_all (fun (_, def) -> not (occur_var env f def)) ldefrec
+             if List.for_all (fun (_, def) -> not (Termops.occur_var env f def)) ldefrec
              then i else failwith "try_find_i")
           0 lnamerec
       in
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 6154b19ad..311889448 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -13,7 +13,6 @@ open Names
 open Sign
 open Evd
 open Term
-open Termops
 open Reductionops
 open Environ
 open Type_errors
@@ -106,7 +105,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
       else id
 
   let invert_ltac_bound_name env id0 id =
-    try mkRel (pi1 (lookup_rel_id id (rel_context env)))
+    try mkRel (pi1 (Termops.lookup_rel_id id (rel_context env)))
     with Not_found ->
       errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++
 	str " depends on pattern variable name " ++ pr_id id ++
@@ -115,7 +114,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
   let pretype_id loc env sigma (lvar,unbndltacvars) id =
     let id = strip_meta id in (* May happen in tactics defined by Grammar *)
       try
-	let (n,_,typ) = lookup_rel_id id (rel_context env) in
+	let (n,_,typ) = Termops.lookup_rel_id id (rel_context env) in
 	  { uj_val  = mkRel n; uj_type = lift n typ }
       with Not_found ->
 	try
@@ -151,7 +150,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
     let s' = mkProd (Anonymous, ind, s) in
     let ccl = lift 1 (decomp n pj.uj_val) in
     let ccl' = mkLambda (Anonymous, ind, ccl) in
-      {uj_val=it_mkLambda ccl' sign; uj_type=it_mkProd s' sign}
+      {uj_val=Termops.it_mkLambda ccl' sign; uj_type=Termops.it_mkProd s' sign}
 
   (*************************************************************************)
   (* Main pretyping function                                               *)
@@ -224,7 +223,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
           match tycon with
             | Some (None, ty) -> ty
             | None | Some _ ->
-		e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ()) in
+		e_new_evar evdref env ~src:(loc, InternalHole) (Termops.new_Type ()) in
 	  { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
 
     | RRec (loc,fixkind,names,bl,lar,vdef) ->
@@ -386,7 +385,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
     | RProd(loc,name,k,c1,c2)        ->
 	let j = pretype_type empty_valcon env evdref lvar c1 in
 	let var = (name,j.utj_val) in
-	let env' = push_rel_assum var env in
+	let env' = Termops.push_rel_assum var env in
 	let j' = pretype_type empty_valcon env' evdref lvar c2 in
 	let resj =
 	  try judge_of_product env name j j'
@@ -395,7 +394,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 
     | RLetIn(loc,name,c1,c2)      ->
 	let j = pretype empty_tycon env evdref lvar c1 in
-	let t = refresh_universes j.uj_type in
+	let t = Termops.refresh_universes j.uj_type in
 	let var = (name,Some j.uj_val,t) in
         let tycon = lift_tycon 1 tycon in
 	let j' = pretype tycon (push_rel var env) evdref lvar c2 in
@@ -503,7 +502,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		let p = match tycon with
 		  | Some (None, ty) -> ty
 		  | None | Some _ ->
-                      e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ())
+                      e_new_evar evdref env ~src:(loc,InternalHole) (Termops.new_Type ())
 		in
 		  it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
 	  let pred = nf_evar ( !evdref) pred in
@@ -584,7 +583,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		 { utj_val = v;
 		   utj_type = s }
 	   | None ->
-	       let s = new_Type_sort () in
+	       let s = Termops.new_Type_sort () in
 		 { utj_val = e_new_evar evdref env ~src:loc (mkSort s);
 		   utj_type = s})
     | c ->
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 689b110f8..106ac4d09 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -414,7 +414,6 @@ let string_of_intset d =
 open Printer
 open Ppconstr
 open Nameops
-open Termops
 open Evd
 
 let pr_meta_map evd =
@@ -426,11 +425,11 @@ let pr_meta_map evd =
     | (mv,Cltyp (na,b)) ->
       	hov 0
 	  (pr_meta mv ++ pr_name na ++ str " : " ++
-           print_constr b.rebus ++ fnl ())
+           Termops.print_constr b.rebus ++ fnl ())
     | (mv,Clval(na,b,_)) ->
       	hov 0
 	  (pr_meta mv ++ pr_name na ++ str " := " ++
-             print_constr (fst b).rebus ++ fnl ())
+             Termops.print_constr (fst b).rebus ++ fnl ())
   in
   prlist pr_meta_binding ml
 
@@ -441,11 +440,11 @@ let pr_evar_info evi =
     (*pr_idl (List.rev (ids_of_named_context (evar_context evi))) *)
     Printer.pr_named_context (Global.env()) (evar_context evi)
   in
-  let pty = print_constr evi.evar_concl in
+  let pty = Termops.print_constr evi.evar_concl in
   let pb =
     match evi.evar_body with
       | Evar_empty -> mt ()
-      | Evar_defined c -> spc() ++ str"=> "  ++ print_constr c
+      | Evar_defined c -> spc() ++ str"=> "  ++ Termops.print_constr c
   in
   hov 2 (str"["  ++ phyps ++ spc () ++ str"|- "  ++ pty ++ pb ++ str"]")
 
@@ -459,11 +458,11 @@ let pr_evar_map sigma =
 let pr_constraints pbs =
   h 0
     (prlist_with_sep pr_fnl (fun (pbty,t1,t2) ->
-      print_constr t1 ++ spc() ++
+      Termops.print_constr t1 ++ spc() ++
       str (match pbty with
 	| Reduction.CONV -> "=="
 	| Reduction.CUMUL -> "<=") ++
-      spc() ++ print_constr t2) pbs)
+      spc() ++ Termops.print_constr t2) pbs)
 
 let pr_evar_map evd =
   let pp_evm =
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 941b6f7df..acded3ac5 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -16,7 +16,6 @@ open Names
 open Libnames
 open Nameops
 open Term
-open Termops
 open Namegen
 open Declarations
 open Entries
@@ -55,7 +54,7 @@ let mis_make_case_com dep env sigma ind (mib,mip as specif) kind =
   if not (List.mem kind (elim_sorts specif)) then
     raise
       (RecursionSchemeError
-	 (NotAllowedCaseAnalysis (false,new_sort_in_family kind,ind)));
+	 (NotAllowedCaseAnalysis (false, Termops.new_sort_in_family kind, ind)));
 
   let ndepar = mip.mind_nrealargs_ctxt + 1 in
 
@@ -63,7 +62,7 @@ let mis_make_case_com dep env sigma ind (mib,mip as specif) kind =
   (* mais pas très joli ... (mais manque get_sort_of à ce niveau) *)
   let env' = push_rel_context lnamespar env in
 
-  let indf = make_ind_family(ind, extended_rel_list 0 lnamespar) in
+  let indf = make_ind_family(ind, Termops.extended_rel_list 0 lnamespar) in
   let constrs = get_constructors env indf in
 
   let rec add_branch env k =
@@ -79,8 +78,8 @@ let mis_make_case_com dep env sigma ind (mib,mip as specif) kind =
       let pbody =
         appvect
           (mkRel (ndepar + nbprod),
-           if dep then extended_rel_vect 0 deparsign
-           else extended_rel_vect 1 arsign) in
+           if dep then Termops.extended_rel_vect 0 deparsign
+           else Termops.extended_rel_vect 1 arsign) in
       let p =
 	it_mkLambda_or_LetIn_name env'
 	  ((if dep then mkLambda_name env' else mkLambda)
@@ -90,7 +89,7 @@ let mis_make_case_com dep env sigma ind (mib,mip as specif) kind =
       it_mkLambda_or_LetIn_name env'
        	(mkCase (ci, lift ndepar p,
 		     mkRel 1,
-		     rel_vect ndepar k))
+		     Termops.rel_vect ndepar k))
        	deparsign
     else
       let cs = lift_constructor (k+1) constrs.(k) in
@@ -98,7 +97,7 @@ let mis_make_case_com dep env sigma ind (mib,mip as specif) kind =
       mkLambda_string "f" t
 	(add_branch (push_rel (Anonymous, None, t) env) (k+1))
   in
-  let typP = make_arity env' dep indf (new_sort_in_family kind) in
+  let typP = make_arity env' dep indf (Termops.new_sort_in_family kind) in
   it_mkLambda_or_LetIn_name env
     (mkLambda_string "P" typP
        (add_branch (push_rel (Anonymous,None,typP) env') 0)) lnamespar
@@ -138,7 +137,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
 	    let base = applist (lift i pk,realargs) in
             if depK then
 	      Reduction.beta_appvect
-                base [|applist (mkRel (i+1),extended_rel_list 0 sign)|]
+                base [|applist (mkRel (i+1), Termops.extended_rel_list 0 sign)|]
             else
 	      base
       	| _ -> assert false
@@ -210,7 +209,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
 	    mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c)
      	| Ind _ ->
             let realargs = list_skipn nparrec largs
-            and arg = appvect (mkRel (i+1),extended_rel_vect 0 hyps) in
+            and arg = appvect (mkRel (i+1), Termops.extended_rel_vect 0 hyps) in
             applist(lift i fk,realargs@[arg])
      	| _ -> assert false
     in
@@ -296,7 +295,7 @@ let mis_make_indrec env sigma listdepkind mib =
 
             (* arity in the context of the fixpoint, i.e.
                P1..P_nrec f1..f_nbconstruct *)
-	    let args = extended_rel_list (nrec+nbconstruct) lnamesparrec in
+	    let args = Termops.extended_rel_list (nrec+nbconstruct) lnamesparrec in
 	    let indf = make_ind_family(indi,args) in
 
 	    let arsign,_ = get_arity env indf in
@@ -310,15 +309,15 @@ let mis_make_indrec env sigma listdepkind mib =
 
             (* constructors in context of the Cases expr, i.e.
                P1..P_nrec f1..f_nbconstruct F_1..F_nrec a_1..a_nar x:I *)
-	    let args' = extended_rel_list (dect+nrec) lnamesparrec in
-	    let args'' = extended_rel_list ndepar lnonparrec in
+	    let args' = Termops.extended_rel_list (dect+nrec) lnamesparrec in
+	    let args'' = Termops.extended_rel_list ndepar lnonparrec in
             let indf' = make_ind_family(indi,args'@args'') in
 
 	    let branches =
 	      let constrs = get_constructors env indf' in
-	      let fi = rel_vect (dect-i-nctyi) nctyi in
+	      let fi = Termops.rel_vect (dect-i-nctyi) nctyi in
 	      let vecfi = Array.map
-		(fun f -> appvect (f,extended_rel_vect ndepar lnonparrec))
+		(fun f -> appvect (f, Termops.extended_rel_vect ndepar lnonparrec))
 		fi
 	      in
 		array_map3
@@ -339,9 +338,9 @@ let mis_make_indrec env sigma listdepkind mib =
 	    let deparsign' = (Anonymous,None,depind')::arsign' in
 
 	    let pargs =
-	      let nrpar = extended_rel_list (2*ndepar) lnonparrec
-	      and nrar = if dep then extended_rel_list 0 deparsign'
-		else extended_rel_list 1 arsign'
+	      let nrpar = Termops.extended_rel_list (2*ndepar) lnonparrec
+	      and nrar = if dep then Termops.extended_rel_list 0 deparsign'
+		else Termops.extended_rel_list 1 arsign'
 	      in nrpar@nrar
 
 	    in
@@ -360,15 +359,15 @@ let mis_make_indrec env sigma listdepkind mib =
 		  (mkCase (ci, pred,
 		          mkRel 1,
 			  branches))
-		  (lift_rel_context nrec deparsign)
+		  (Termops.lift_rel_context nrec deparsign)
 	    in
 
 	    (* type of i-th component of the mutual fixpoint *)
 
 	    let typtyi =
 	      let concl =
-		let pargs = if dep then extended_rel_vect 0 deparsign
-		  else extended_rel_vect 1 arsign
+		let pargs = if dep then Termops.extended_rel_vect 0 deparsign
+		  else Termops.extended_rel_vect 1 arsign
 		in appvect (mkRel (nbconstruct+ndepar+nonrecpar+j),pargs)
 	      in it_mkProd_or_LetIn_name env
 		concl
@@ -395,7 +394,7 @@ let mis_make_indrec env sigma listdepkind mib =
 	    else
 	      let recarg = (dest_subterms recargsvec.(tyi)).(j) in
 	      let recarg = recargpar@recarg in
-	      let vargs = extended_rel_list (nrec+i+j) lnamesparrec in
+	      let vargs = Termops.extended_rel_list (nrec+i+j) lnamesparrec in
 	      let cs = get_constructor (indi,mibi,mipi,vargs) (j+1) in
 	      let p_0 =
 		type_rec_branch
@@ -409,8 +408,8 @@ let mis_make_indrec env sigma listdepkind mib =
     in
     let rec put_arity env i = function
       | (indi,_,_,dep,kinds)::rest ->
-	  let indf = make_ind_family (indi,extended_rel_list i lnamesparrec) in
-	  let typP = make_arity env dep indf (new_sort_in_family kinds) in
+	  let indf = make_ind_family (indi, Termops.extended_rel_list i lnamesparrec) in
+	  let typP = make_arity env dep indf (Termops.new_sort_in_family kinds) in
 	    mkLambda_string "P" typP
 	      (put_arity (push_rel (Anonymous,None,typP) env) (i+1) rest)
       | [] ->
@@ -504,7 +503,7 @@ let check_arities listdepkind =
        let kelim = elim_sorts (mibi,mipi) in
        if not (List.exists ((=) kind) kelim) then raise
 	 (RecursionSchemeError
-	   (NotAllowedCaseAnalysis (true,new_sort_in_family kind,mind)))
+	   (NotAllowedCaseAnalysis (true, Termops.new_sort_in_family kind,mind)))
        else if List.mem ni ln then raise
 	 (RecursionSchemeError (NotMutualInScheme (mind,mind)))
        else ni::ln)
@@ -569,5 +568,5 @@ let lookup_eliminator ind_sp s =
       (strbrk "Cannot find the elimination combinator " ++
        pr_id id ++ strbrk ", the elimination of the inductive definition " ++
        pr_global_env Idset.empty (IndRef ind_sp) ++
-       strbrk " on sort " ++ pr_sort_family s ++
+       strbrk " on sort " ++ Termops.pr_sort_family s ++
        strbrk " is probably not allowed.")
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index d477ec34a..ccedf1520 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -19,7 +19,6 @@ open Names
 open Libnames
 open Nametab
 open Term
-open Termops
 open Typeops
 open Libobject
 open Library
@@ -206,7 +205,7 @@ let cs_pattern_of_constr t =
 	      _ -> raise Not_found
 	end
     | Rel n -> Default_cs, pred n, []
-    | Prod (_,a,b) when not (dependent (mkRel 1) b) -> Prod_cs, -1, [a;pop b]
+    | Prod (_,a,b) when not (Termops.dependent (mkRel 1) b) -> Prod_cs, -1, [a; Termops.pop b]
     | Sort s -> Sort_cs (family_of_sort s), -1, []
     | _ ->
 	begin
@@ -240,7 +239,7 @@ let compute_canonical_projections (con,ind) =
                      (let con_pp = Nametab.pr_global_env Idset.empty (ConstRef con)
                       and proji_sp_pp = Nametab.pr_global_env Idset.empty (ConstRef proji_sp) in
 		      msg_warning (str "No global reference exists for projection value"
-                                   ++ print_constr t ++ str " in instance "  
+                                   ++ Termops.print_constr t ++ str " in instance "  
                                    ++ con_pp ++ str " of " ++ proji_sp_pp ++ str ", ignoring it."));
 		   l
 	       end
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 49ff459c6..8955b6c7e 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -18,7 +18,6 @@ open Tacexpr
 open Rawterm
 open Tactics
 open Util
-open Termops
 open Evd
 open Equality
 open Compat
@@ -228,11 +227,11 @@ TACTIC EXTEND rewrite_star
 | [ "rewrite" "*" orient(o) open_constr(c) "at" occurrences(occ) "in" hyp(id) by_arg_tac(tac) ] ->
     [ rewrite_star (Some id) o (occurrences_of occ) c tac ]
 | [ "rewrite" "*" orient(o) open_constr(c) "in" hyp(id) by_arg_tac(tac) ] ->
-    [ rewrite_star (Some id) o all_occurrences c tac ]
+    [ rewrite_star (Some id) o Termops.all_occurrences c tac ]
 | [ "rewrite" "*" orient(o) open_constr(c) "at" occurrences(occ) by_arg_tac(tac) ] ->
     [ rewrite_star None o (occurrences_of occ) c tac ]
 | [ "rewrite" "*" orient(o) open_constr(c) by_arg_tac(tac) ] ->
-    [ rewrite_star None o all_occurrences c tac ]
+    [ rewrite_star None o Termops.all_occurrences c tac ]
     END
 
 (**********************************************************************)
@@ -538,7 +537,7 @@ END
 (**********************************************************************)
 
 let subst_var_with_hole occ tid t = 
-  let occref = if occ > 0 then ref occ else error_invalid_occurrence [occ] in
+  let occref = if occ > 0 then ref occ else Termops.error_invalid_occurrence [occ] in
   let locref = ref 0 in
   let rec substrec = function
     | RVar (_,id) as x -> 
@@ -549,7 +548,7 @@ let subst_var_with_hole occ tid t =
     | c -> map_rawconstr_left_to_right substrec c in
   let t' = substrec t
   in
-  if !occref > 0 then error_invalid_occurrence [occ] else t'
+  if !occref > 0 then Termops.error_invalid_occurrence [occ] else t'
 
 let subst_hole_with_term occ tc t =
   let locref = ref 0 in
@@ -570,9 +569,9 @@ let out_arg = function
 
 let hResolve id c occ t gl = 
   let sigma = project gl in 
-  let env = clear_named_body id (pf_env gl) in
-  let env_ids = ids_of_context env in
-  let env_names = names_of_rel_context env in
+  let env = Termops.clear_named_body id (pf_env gl) in
+  let env_ids = Termops.ids_of_context env in
+  let env_names = Termops.names_of_rel_context env in
   let c_raw = Detyping.detype true env_ids env_names c in 
   let t_raw = Detyping.detype true env_ids env_names t in 
   let rec resolve_hole t_hole =
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 821fc0fad..09b983622 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -10,7 +10,6 @@
 open Names
 open Decl_kinds
 open Term
-open Termops
 open Sign
 open Entries
 open Evd
diff --git a/toplevel/record.ml b/toplevel/record.ml
index b87d11d54..b751db85b 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -12,7 +12,6 @@ open Names
 open Libnames
 open Nameops
 open Term
-open Termops
 open Environ
 open Declarations
 open Entries
@@ -59,7 +58,7 @@ let typecheck_params_and_fields id t ps nots fs =
   let env0 = Global.env () in
   let evars = ref Evd.empty in
   let (env1,newps), imps = interp_context_evars evars env0 ps in
-  let fullarity = it_mkProd_or_LetIn (Option.cata (fun x -> x) (new_Type ()) t) newps in
+  let fullarity = it_mkProd_or_LetIn (Option.cata (fun x -> x) (Termops.new_Type ()) t) newps in
   let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
   let env2,impls,newfs,data =
     interp_fields_evars evars env_ar nots (binders_of_decls fs)
@@ -148,7 +147,7 @@ let subst_projection fid l c =
 
 let instantiate_possibly_recursive_type indsp paramdecls fields =
   let subst = list_map_i (fun i _ -> mkRel i) 1 paramdecls in
-  substl_rel_context (subst@[mkInd indsp]) fields
+  Termops.substl_rel_context (subst@[mkInd indsp]) fields
 
 (* We build projections *)
 let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls fields =
@@ -156,11 +155,11 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
   let (mib,mip) = Global.lookup_inductive indsp in
   let paramdecls = mib.mind_params_ctxt in
   let r = mkInd indsp in
-  let rp = applist (r, extended_rel_list 0 paramdecls) in
-  let paramargs = extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*)
+  let rp = applist (r, Termops.extended_rel_list 0 paramdecls) in
+  let paramargs = Termops.extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*)
   let x = match name with Some n -> Name n | None -> Namegen.named_hd (Global.env()) r Anonymous in
   let fields = instantiate_possibly_recursive_type indsp paramdecls fields in
-  let lifted_fields = lift_rel_context 1 fields in
+  let lifted_fields = Termops.lift_rel_context 1 fields in
   let (_,kinds,sp_projs,_) =
     list_fold_left3
       (fun (nfi,kinds,sp_projs,subst) coe (fi,optci,ti) impls ->
@@ -234,7 +233,7 @@ open Typeclasses
 let declare_structure finite infer id idbuild paramimpls params arity fieldimpls fields
     ?(kind=StructureComponent) ?name is_coe coers sign =
   let nparams = List.length params and nfields = List.length fields in
-  let args = extended_rel_list nfields params in
+  let args = Termops.extended_rel_list nfields params in
   let ind = applist (mkRel (1+nparams+nfields), args) in
   let type_constructor = it_mkProd_or_LetIn ind fields in
   let mie_ind =
@@ -248,7 +247,7 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls
   (* there is probably a way to push this to "declare_mutual" *)
   begin match  finite with
   | BiFinite ->
-      if dependent (mkRel (nparams+1)) (it_mkProd_or_LetIn mkProp fields) then
+      if Termops.dependent (mkRel (nparams+1)) (it_mkProd_or_LetIn mkProp fields) then
 	error "Records declared with the keyword Record or Structure cannot be recursive. Maybe you meant to define an Inductive or CoInductive record."
   | _ -> ()
   end;
@@ -306,7 +305,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
 	let cst = Declare.declare_constant (snd id)
 	  (DefinitionEntry class_entry, IsDefinition Definition)
 	in
-	let inst_type = appvectc (mkConst cst) (rel_vect 0 (List.length params)) in
+	let inst_type = appvectc (mkConst cst) (Termops.rel_vect 0 (List.length params)) in
 	let proj_type = it_mkProd_or_LetIn (mkProd(Name (snd id), inst_type, lift 1 field)) params in
 	let proj_body = it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in
 	let proj_entry =
@@ -325,9 +324,9 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
 	if infer then Evd.fold (fun ev evi _ -> Recordops.declare_method (ConstRef cst) ev sign) sign ();
 	cref, [proj_name, Some proj_cst]
     | _ ->
-	let idarg = Namegen.next_ident_away (snd id) (ids_of_context (Global.env())) in
+	let idarg = Namegen.next_ident_away (snd id) (Termops.ids_of_context (Global.env())) in
 	let ind = declare_structure BiFinite infer (snd id) idbuild paramimpls
-	  params (Option.cata (fun x -> x) (new_Type ()) arity) fieldimpls fields
+	  params (Option.cata (fun x -> x) (Termops.new_Type ()) arity) fieldimpls fields
 	  ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) sign
 	in
 	  IndRef ind, (List.map2 (fun (id, _, _) y -> (Nameops.out_name id, y))
@@ -385,7 +384,7 @@ let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuil
 	if infer then search_record declare_class_instance gr sign;
 	gr
     | _ ->
-	let arity = Option.default (new_Type ()) sc in
+	let arity = Option.default (Termops.new_Type ()) sc in
 	let implfs = List.map
 	  (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in
 	let ind = declare_structure finite infer idstruc idbuild implpars params arity implfs fields is_coe coers sign in
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index f597773fa..906629997 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -18,7 +18,6 @@ open Environ
 open Rawterm
 open Libnames
 open Nametab
-open Termops
 open Detyping
 open Constrintern
 open Dischargedhypsmap
@@ -196,7 +195,7 @@ let whelp_elim ind =
 let on_goal f =
   let { Evd.it=goals ; sigma=sigma } = Proof.V82.subgoals (get_pftreestate ()) in
   let gls = { Evd.it=List.hd goals ; sigma = sigma }  in
-  f (it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls))
+  f (Termops.it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls))
 
 type whelp_request =
   | Locate of string