From 4b68dbe3428740a61cda825d3a45047571d9f299 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Sat, 1 Mar 2014 19:50:59 +0100
Subject: 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
---
 interp/notation_ops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index f6afbe48a4..12b256c453 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
 
-- 
cgit v1.2.3