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

1 files changed, 9 insertions, 10 deletions

diff --git a/parsing/printer.ml b/parsing/printer.ml
index 34637b1e83..c575fde52b 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,_) ->