aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/constr_matching.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/constr_matching.ml')
-rw-r--r--pretyping/constr_matching.ml13
1 files changed, 8 insertions, 5 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index cad21543b..30b83cf88 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -205,11 +205,14 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
| PRel n1, Rel n2 when Int.equal n1 n2 -> subst
- | PSort GProp, Sort (Prop Null) -> subst
-
- | PSort GSet, Sort (Prop Pos) -> subst
-
- | PSort (GType _), Sort (Type _) -> subst
+ | PSort ps, Sort s ->
+
+ begin match ps, ESorts.kind sigma s with
+ | GProp, Prop Null -> subst
+ | GSet, Prop Pos -> subst
+ | GType _, Type _ -> subst
+ | _ -> raise PatternMatchingFailure
+ end
| PApp (p, [||]), _ -> sorec ctx env subst p t