From 26a79004e47bbdc97df61015ce7e944eef14ac71 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 8 Sep 2014 10:23:12 +0200
Subject: Parsing of Type@{max(i,j)}.

---
 interp/notation_ops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 5cad2b54d6..9461cebb0f 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -731,7 +731,7 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
       match_in u alp metas (match_in u alp metas sigma c1 c2) t1 t2
   | GCast(_,c1, CastCoerce), NCast(c2, CastCoerce) ->
       match_in u alp metas sigma c1 c2
-  | GSort (_,GType _), NSort (GType None) when not u -> sigma
+  | GSort (_,GType _), NSort (GType _) when not u -> 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