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

4 files changed, 39 insertions, 43 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index bc12fcea9c..43658e8021 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 e0b08599d0..6034f19e65 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 f0ea133c60..24382f8753 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 e329196acc..c42ecac421 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));;