From 460bf801123d13e8c82503a2fc491892f8eed6d5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 14 Nov 2018 10:10:39 +0100
Subject: Allowing Set to be part of universe expressions.

Conversely, Type existential variables now (explicitly) cover the Set
case.

Similarly for Prop and SProp.
---
 interp/notation_ops.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 7f084fffdd..08619d912e 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1190,7 +1190,11 @@ let rec match_ inner u alp metas sigma a1 a2 =
       Array.fold_left2 (match_in u alp metas) sigma bl1 bl2
   | GCast(t1, c1), NCast(t2, c2) ->
     match_cast (match_in u alp metas) (match_in u alp metas sigma t1 t2) c1 c2
-  | GSort (GType _), NSort (GType _) when not u -> sigma
+
+  (* Next pair of lines useful only if not coming from detyping *)
+  | GSort (UNamed [(GProp|GSet),0]), NSort (UAnonymous _) -> raise No_match
+  | GSort _, NSort (UAnonymous _) when not u -> sigma
+
   | GSort s1, NSort s2 when glob_sort_eq s1 s2 -> sigma
   | GInt i1, NInt i2 when Uint63.equal i1 i2 -> sigma
   | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
-- 
cgit v1.2.3