diff options
Diffstat (limited to 'pretyping/constr_matching.ml')
| -rw-r--r-- | pretyping/constr_matching.ml | 13 |
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 |