Glob_term now mli-only, operations now in Glob_ops

Stuff about reductions now in genredexpr.mli, operations in redops.ml

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

6 files changed, 7 insertions, 2 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index d45e6b9b37..62b8cdcea8 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -23,6 +23,7 @@ open Libnames
 open Impargs
 open Topconstr
 open Glob_term
+open Glob_ops
 open Pattern
 open Nametab
 open Notation
@@ -876,7 +877,7 @@ and extern_eqn inctx scopes vars (loc,ids,pl,c) =
 and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
   | [] -> raise No_match
   | (keyrule,pat,n as _rule)::rules ->
-      let loc = Glob_term.loc_of_glob_constr t in
+      let loc = Glob_ops.loc_of_glob_constr t in
       try
 	(* Adjusts to the number of arguments expected by the notation *)
 	let (t,args,argsscopes,argsimpls) = match t,n with
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4467cf9f24..d125caf546 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -16,6 +16,7 @@ open Namegen
 open Libnames
 open Impargs
 open Glob_term
+open Glob_ops
 open Pattern
 open Pretyping
 open Cases
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index b1bc63658b..250871b9e0 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -82,7 +82,7 @@ val intern_gen : bool -> evar_map -> env ->
 
 val intern_pattern : env -> cases_pattern_expr ->
   Names.identifier list *
-    ((Names.identifier * Names.identifier) list * Glob_term.cases_pattern) list
+    ((Names.identifier * Names.identifier) list * cases_pattern) list
 
 val intern_context : bool -> evar_map -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list
 
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 0368e99e02..de1fa0fef6 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -12,6 +12,7 @@ open Names
 open Term
 open Libnames
 open Glob_term
+open Genredexpr
 open Pattern
 open Topconstr
 open Term
diff --git a/interp/notation.ml b/interp/notation.ml
index 72a7138669..b6496f535a 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -17,6 +17,7 @@ open Nametab
 open Libnames
 open Summary
 open Glob_term
+open Glob_ops
 open Topconstr
 open Ppextend
 (*i*)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index d3773305a7..9ea6c7e4c5 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -14,6 +14,7 @@ open Names
 open Nameops
 open Libnames
 open Glob_term
+open Glob_ops
 open Term
 open Mod_subst
 open Misctypes