diff options
| author | Gaëtan Gilbert | 2019-03-17 10:40:31 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-18 12:52:42 +0100 |
| commit | a71f586e23b0e68032c556bfa1c37df8f4358c71 (patch) | |
| tree | 876772675b8bcf7cfa3d4ff2b7ea460c62ebd04f /pretyping/constr_matching.ml | |
| parent | 9ac5483132b42e845a0708491843693b70893eef (diff) | |
Fix constr_matching on SProp
Diffstat (limited to 'pretyping/constr_matching.ml')
| -rw-r--r-- | pretyping/constr_matching.ml | 11 |
1 files changed, 2 insertions, 9 deletions
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 |