Merge PR #9791: Fix constr_matching on SProp

Ack-by: SkySkimmer
Reviewed-by: ppedrot

6 files changed, 21 insertions, 21 deletions

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 =
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index bc083ed9d9..6bfbb9a9c0 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -17,7 +17,6 @@ open Constr
 open Context
 open Globnames
 open Termops
-open Term
 open EConstr
 open Vars
 open Pattern
@@ -280,14 +279,8 @@ let matches_core env sigma allow_bound_rels
       | PRel n1, Rel n2 when Int.equal n1 n2 -> subst
 
       | PSort ps, Sort s ->
-
-        let open Glob_term in
-        begin match ps, ESorts.kind sigma s with
-        | GProp, Prop -> subst
-        | GSet, Set -> subst
-        | GType _, Type _ -> subst
-        | _ -> raise PatternMatchingFailure
-        end
+        if Sorts.family_equal ps (Sorts.family (ESorts.kind sigma s))
+        then subst else raise PatternMatchingFailure
 
       | PApp (p, [||]), _ -> sorec ctx env subst p t
 
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index affed5389f..74432cc010 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -47,11 +47,18 @@ let map_glob_decl_left_to_right f (na,k,obd,ty) =
 
 
 let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with
-| GProp, GProp -> true
+| GSProp, GSProp
+| GProp, GProp
 | GSet, GSet -> true
 | GType l1, GType l2 ->
    List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.qualid_eq x y && Int.equal m n)) l1 l2
-| _ -> false
+| (GSProp|GProp|GSet|GType _), _ -> false
+
+let glob_sort_family = let open Sorts in function
+| GSProp -> InSProp
+| GProp -> InProp
+| GSet -> InSet
+| GType _ -> InType
 
 let binding_kind_eq bk1 bk2 = match bk1, bk2 with
   | Decl_kinds.Explicit, Decl_kinds.Explicit -> true
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index c189a3bcb2..2f0ac76235 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -15,6 +15,8 @@ open Glob_term
 
 val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool
 
+val glob_sort_family : 'a glob_sort_gen -> Sorts.family
+
 val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool
 
 val alias_of_pat : 'a cases_pattern_g -> Name.t
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 2ca7f21e8d..d1c0a4ea2a 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -32,7 +32,7 @@ type constr_pattern =
   | PLambda of Name.t * constr_pattern * constr_pattern
   | PProd of Name.t * constr_pattern * constr_pattern
   | PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern
-  | PSort of Glob_term.glob_sort
+  | PSort of Sorts.family
   | PMeta of patvar option
   | PIf of constr_pattern * constr_pattern * constr_pattern
   | PCase of case_info_pattern * constr_pattern * constr_pattern *
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 13034d078a..4e3c77cb1a 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -13,7 +13,6 @@ open Util
 open Names
 open Globnames
 open Nameops
-open Term
 open Constr
 open Context
 open Glob_term
@@ -47,7 +46,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
 | PLetIn (v1, b1, t1, c1), PLetIn (v2, b2, t2, c2) ->
   Name.equal v1 v2 && constr_pattern_eq b1 b2 &&
   Option.equal constr_pattern_eq t1 t2 && constr_pattern_eq c1 c2
-| PSort s1, PSort s2 -> Glob_ops.glob_sort_eq s1 s2
+| PSort s1, PSort s2 -> Sorts.family_equal 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
@@ -154,10 +153,7 @@ let pattern_of_constr env sigma t =
     | Rel n  -> PRel n
     | Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n)))
     | Var id -> PVar id
-    | Sort SProp -> PSort GSProp
-    | Sort Prop -> PSort GProp
-    | Sort Set -> PSort GSet
-    | Sort (Type _) -> PSort (GType [])
+    | Sort s -> PSort (Sorts.family s)
     | Cast (c,_,_)      -> pattern_of_constr env c
     | LetIn (na,c,t,b) -> PLetIn (na.binder_name,
                                   pattern_of_constr env c,Some (pattern_of_constr env t),
@@ -416,8 +412,7 @@ 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 s ->
-      PSort s
+  | GSort gs -> PSort (Glob_ops.glob_sort_family gs)
   | GHole _ ->
       PMeta None
   | GCast (c,_) ->