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
---
 pretyping/patternops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/patternops.ml')

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
-- 
cgit v1.2.3