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, 15 insertions, 19 deletions

diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 93f9b586bc..31e6307415 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 634a6ea600..397bda9b02 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 6154b19adf..3118894482 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 689b110f8a..106ac4d091 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 =