From a71f586e23b0e68032c556bfa1c37df8f4358c71 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sun, 17 Mar 2019 10:40:31 +0100
Subject: Fix constr_matching on SProp

---
 interp/constrextern.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index d5cb25d1fb..c2afa097bb 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1314,7 +1314,10 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
           Array.map (fun (bl,_,_) -> bl) v,
           Array.map (fun (_,_,ty) -> ty) v,
           Array.map (fun (_,bd,_) -> bd) v)
-  | PSort s -> GSort s
+  | PSort Sorts.InSProp -> GSort GSProp
+  | PSort Sorts.InProp -> GSort GProp
+  | PSort Sorts.InSet -> GSort GSet
+  | PSort Sorts.InType -> GSort (GType [])
   | PInt i -> GInt i
 
 let extern_constr_pattern env sigma pat =
-- 
cgit v1.2.3