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

(limited to 'pretyping/patternops.ml')

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index c788efda48..2d27b27cab 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -410,7 +410,9 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
       PLetIn (na, pat_of_raw metas vars c1,
                Option.map (pat_of_raw metas vars) t,
 	       pat_of_raw metas (na::vars) c2)
-  | GSort gs -> PSort (Glob_ops.glob_sort_family gs)
+  | GSort gs ->
+     (try PSort (Glob_ops.glob_sort_family gs)
+      with Glob_ops.ComplexSort -> user_err ?loc (str "Unexpected universe in pattern."))
   | GHole _ ->
       PMeta None
   | GCast (c,_) ->
-- 
cgit v1.2.3