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, 11 insertions, 56 deletions

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 9fc981a7d2..f1e38d0f8f 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -46,13 +46,6 @@ let case_style_eq s1 s2 = match s1, s2 with
 | RegularStyle, RegularStyle -> true
 | _ -> false
 
-let glob_sort_eq g1 g2 = match g1, g2 with
-| GProp, GProp -> true
-| GSet, GSet -> true
-| GType None, GType None -> true
-| GType (Some s1), GType (Some s2) -> String.equal s1 s2
-| _ -> false
-
 let rec cases_pattern_eq p1 p2 = match p1, p2 with
 | PatVar (_, na1), PatVar (_, na2) -> Name.equal na1 na2
 | PatCstr (_, c1, pl1, na1), PatCstr (_, c2, pl2, na2) ->
@@ -67,13 +60,6 @@ let cast_type_eq eq t1 t2 = match t1, t2 with
 | CastNative t1, CastNative t2 -> eq t1 t2
 | _ -> false
 
-let eq_gr gr1 gr2 = match gr1, gr2 with
-| ConstRef con1, ConstRef con2 -> eq_constant con1 con2
-| IndRef kn1, IndRef kn2 -> eq_ind kn1 kn2
-| ConstructRef kn1, ConstructRef kn2 -> eq_constructor kn1 kn2
-| VarRef v1, VarRef v2 -> Id.equal v1 v2
-| _ -> false
-
 let rec glob_constr_eq c1 c2 = match c1, c2 with
 | GRef (_, gr1), GRef (_, gr2) -> eq_gr gr1 gr2
 | GVar (_, id1), GVar (_, id2) -> Id.equal id1 id2
@@ -109,7 +95,7 @@ let rec glob_constr_eq c1 c2 = match c1, c2 with
   Array.equal (fun l1 l2 -> List.equal glob_decl_eq l1 l2) decl1 decl2 &&
   Array.equal glob_constr_eq c1 c2 &&
   Array.equal glob_constr_eq t1 t2
-| GSort (_, s1), GSort (_, s2) -> glob_sort_eq s1 s2
+| GSort (_, s1), GSort (_, s2) -> Miscops.glob_sort_eq s1 s2
 | GHole (_, kn1, gn1), GHole (_, kn2, gn2) ->
   Option.equal (==) gn1 gn2 (** Only thing sensible *)
 | GCast (_, c1, t1), GCast (_, c2, t2) ->
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 5195b98c87..1785c87be8 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -18,7 +18,6 @@ open Locus
 open Glob_term
 
 (** Equalities *)
-val glob_sort_eq : glob_sort -> glob_sort -> bool
 
 val cases_pattern_eq : cases_pattern -> cases_pattern -> bool
 
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 2639e2e720..ab01065b19 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -7,8 +7,6 @@
 (************************************************************************)
 
 open Misctypes
-open Pp
-open Nameops
 
 (** Mapping [cast_type] *)
 
@@ -25,33 +23,11 @@ let smartmap_cast_type f c =
     | CastCoerce -> CastCoerce
     | CastNative a -> let a' = f a in if a' == a then c else CastNative a'
 
-(** Printing of [intro_pattern] *)
+(** Equalities on [glob_sort] *)
 
-let rec pr_intro_pattern (_,pat) = match pat with
-  | IntroOrAndPattern pll -> pr_or_and_intro_pattern pll
-  | IntroInjection pl ->
-      str "[=" ++ hv 0 (prlist_with_sep spc pr_intro_pattern pl) ++ str "]"
-  | IntroWildcard -> str "_"
-  | IntroRewrite true -> str "->"
-  | IntroRewrite false -> str "<-"
-  | IntroIdentifier id -> pr_id id
-  | IntroFresh id -> str "?" ++ pr_id id
-  | IntroForthcoming true -> str "*"
-  | IntroForthcoming false -> str "**"
-  | IntroAnonymous -> str "?"
-
-and pr_or_and_intro_pattern = function
-  | [pl] ->
-      str "(" ++ hv 0 (prlist_with_sep pr_comma pr_intro_pattern pl) ++ str ")"
-  | pll ->
-      str "[" ++
-      hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
-      ++ str "]"
-
-(** Printing of [move_location] *)
-
-let pr_move_location pr_id = function
-  | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id
-  | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id
-  | MoveFirst -> str " at top"
-  | MoveLast -> str " at bottom"
+let glob_sort_eq g1 g2 = match g1, g2 with
+| GProp, GProp -> true
+| GSet, GSet -> true
+| GType None, GType None -> true
+| GType (Some s1), GType (Some s2) -> CString.equal s1 s2
+| _ -> false
diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli
index cf984113f6..84541a3b2a 100644
--- a/pretyping/miscops.mli
+++ b/pretyping/miscops.mli
@@ -13,12 +13,6 @@ open Misctypes
 val map_cast_type : ('a -> 'b) -> 'a cast_type -> 'b cast_type
 val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type
 
-(** Printing of [intro_pattern] *)
+(** Equalities on [glob_sort] *)
 
-val pr_intro_pattern : intro_pattern_expr Loc.located -> Pp.std_ppcmds
-val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds
-
-(** Printing of [move_location] *)
-
-val pr_move_location :
-  ('a -> Pp.std_ppcmds) -> 'a move_location -> Pp.std_ppcmds
+val glob_sort_eq : glob_sort -> glob_sort -> bool
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index a2e8e45996..cc13d342a5 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -45,7 +45,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
   Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2
 | PLetIn (v1, t1, b1), PLetIn (v2, t2, b2) ->
   Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2
-| PSort s1, PSort s2 -> glob_sort_eq s1 s2
+| PSort s1, PSort s2 -> Miscops.glob_sort_eq s1 s2
 | PMeta m1, PMeta m2 -> Option.equal Id.equal m1 m2
 | PIf (t1, l1, r1), PIf (t2, l2, r2) ->
   constr_pattern_eq t1 t2 && constr_pattern_eq l1 l2 && constr_pattern_eq r1 r2