diff options
Diffstat (limited to 'pretyping/matching.ml')
| -rw-r--r-- | pretyping/matching.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/matching.ml b/pretyping/matching.ml index fc56f31d3..1facb7c7a 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -173,9 +173,9 @@ let matches_core convert allow_partial_app allow_bound_rels pat c = | PRel n1, Rel n2 when n1 = n2 -> subst - | PSort (RProp c1), Sort (Prop c2) when c1 = c2 -> subst + | PSort (GProp c1), Sort (Prop c2) when c1 = c2 -> subst - | PSort (RType _), Sort (Type _) -> subst + | PSort (GType _), Sort (Type _) -> subst | PApp (p, [||]), _ -> sorec stk subst p t |