Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code

 NB: new file miscprint.ml deserves to be part of printing.cma,
 but should be part of proofs.cma for the moment, due to use in logic.ml

5 files changed, 18 insertions, 25 deletions

diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index 1654d2719..c49b61ce7 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -10,7 +10,6 @@
     of Genarg in [constr]-related interfaces. *)
 
 open Loc
-open Pp
 open Names
 open Term
 open Libnames
@@ -20,9 +19,7 @@ open Genredexpr
 open Pattern
 open Constrexpr
 open Tacexpr
-open Term
 open Misctypes
-open Evd
 open Genarg
 
 (** FIXME: nothing to do there. *)
@@ -53,17 +50,18 @@ val wit_constr_may_eval :
   (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval,
   constr) genarg_type
 
-val wit_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type
+val wit_open_constr :
+  (open_constr_expr, open_glob_constr, Evd.open_constr) genarg_type
 
 val wit_constr_with_bindings :
   (constr_expr with_bindings,
   glob_constr_and_expr with_bindings,
-  constr with_bindings sigma) genarg_type
+  constr with_bindings Evd.sigma) genarg_type
 
 val wit_bindings :
   (constr_expr bindings,
   glob_constr_and_expr bindings,
-  constr bindings sigma) genarg_type
+  constr bindings Evd.sigma) genarg_type
 
 val wit_red_expr :
   ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index c8a0e5638..85ad1cee7 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -10,7 +10,6 @@ open Pp
 open Util
 open Names
 open Libnames
-open Glob_term
 open Constrexpr
 open Misctypes
 open Decl_kinds
@@ -150,7 +149,7 @@ let rec constr_expr_eq e1 e2 =
     Evar.equal ev1 ev2 &&
     Option.equal (List.equal constr_expr_eq) c1 c2
   | CSort(_,s1), CSort(_,s2) ->
-    Glob_ops.glob_sort_eq s1 s2
+    Miscops.glob_sort_eq s1 s2
   | CCast(_,a1,(CastConv b1|CastVM b1)), CCast(_,a2,(CastConv b2|CastVM b2)) ->
       constr_expr_eq a1 a2 &&
       constr_expr_eq b1 b2
@@ -336,14 +335,3 @@ let coerce_to_name = function
   | a -> Errors.user_err_loc
         (constr_loc a,"coerce_to_name",
          str "This expression should be a name.")
-
-let rec raw_cases_pattern_expr_of_glob_constr looked_for = function
-  | GVar (loc,id) -> RCPatAtom (loc,Some id)
-  | GHole (loc,_,_) -> RCPatAtom (loc,None)
-  | GRef (loc,g) ->
-    looked_for g;
-    RCPatCstr (loc, g,[],[])
-  | GApp (loc,GRef (_,g),l) ->
-    looked_for g;
-    RCPatCstr (loc, g,List.map (raw_cases_pattern_expr_of_glob_constr looked_for) l,[])
-  | _ -> raise Not_found
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index d857a5b60..687f5cb9e 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -82,6 +82,3 @@ val names_of_local_binders : local_binder list -> Name.t located list
 val names_of_local_assums : local_binder list -> Name.t located list
 (** Same as [names_of_local_binders], but does not take the [let] bindings into
     account. *)
-
-val raw_cases_pattern_expr_of_glob_constr : (Globnames.global_reference -> unit)
-  -> Glob_term.glob_constr -> raw_cases_pattern_expr
diff --git a/interp/notation.ml b/interp/notation.ml
index 867e23395..262cbab2f 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -449,8 +449,18 @@ let interp_prim_token_gen g loc p local_scopes =
 let interp_prim_token =
   interp_prim_token_gen (fun x -> x)
 
+(** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
+
+let rec rcp_of_glob looked_for = function
+  | GVar (loc,id) -> RCPatAtom (loc,Some id)
+  | GHole (loc,_,_) -> RCPatAtom (loc,None)
+  | GRef (loc,g) -> looked_for g; RCPatCstr (loc, g,[],[])
+  | GApp (loc,GRef (_,g),l) ->
+    looked_for g; RCPatCstr (loc, g, List.map (rcp_of_glob looked_for) l,[])
+  | _ -> raise Not_found
+
 let interp_prim_token_cases_pattern_expr loc looked_for p =
-  interp_prim_token_gen (Constrexpr_ops.raw_cases_pattern_expr_of_glob_constr looked_for) loc p
+  interp_prim_token_gen (rcp_of_glob looked_for) loc p
 
 let interp_notation loc ntn local_scopes =
   let scopes = make_current_scopes local_scopes in
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index f6afbe48a..12b256c45 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -156,7 +156,7 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with
     when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
       on_true_do (f ty1 ty2 && f c1 c2) add na1
   | GHole _, GHole _ -> true
-  | GSort (_,s1), GSort (_,s2) -> glob_sort_eq s1 s2
+  | GSort (_,s1), GSort (_,s2) -> Miscops.glob_sort_eq s1 s2
   | GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when Name.equal na1 na2 ->
       on_true_do (f b1 b2 && f c1 c2) add na1
   | (GCases _ | GRec _
@@ -721,7 +721,7 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
   | GCast(_,c1, CastCoerce), NCast(c2, CastCoerce) ->
       match_in u alp metas sigma c1 c2
   | GSort (_,GType _), NSort (GType None) when not u -> sigma
-  | GSort (_,s1), NSort s2 when glob_sort_eq s1 s2 -> sigma
+  | GSort (_,s1), NSort s2 when Miscops.glob_sort_eq s1 s2 -> sigma
   | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
   | a, NHole _ -> sigma