diff options
| author | Enrico Tassi | 2015-08-24 07:53:57 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2015-08-24 07:53:57 +0200 |
| commit | 14c940b332512f313b0b80acd6a17f80721b32fc (patch) | |
| tree | 517889e5326d90cbab408f7adb5cfaecf19b455e | |
| parent | e9163a8339e8c820a127a4a383b0c9427b11cc2a (diff) | |
Compare pattern heads (constants) up to "univs"
So that Universe Polymorphic constants are compared "correctly",
i.e. not discriminated by the pattern filtering phase (verbatim
head comparison) but eventually by unification.
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 index effd193..c47c946 100644 --- a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 +++ b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 @@ -537,8 +537,8 @@ let filter_upat i0 f n u fpats = let na = Array.length u.up_a in if n < na then fpats else let np = match u.up_k with - | KpatConst when Term.eq_constr u.up_f f -> na - | KpatFixed when Term.eq_constr u.up_f f -> na + | KpatConst when Term.eq_constr_nounivs u.up_f f -> na + | KpatFixed when Term.eq_constr_nounivs u.up_f f -> na | KpatEvar k when isEvar_k k f -> na | KpatLet when isLetIn f -> na | KpatLam when isLambda f -> na @@ -554,8 +554,8 @@ let filter_upat_FO i0 f n u fpats = let np = nb_args u.up_FO in if n < np then fpats else let ok = match u.up_k with - | KpatConst -> Term.eq_constr u.up_f f - | KpatFixed -> Term.eq_constr u.up_f f + | KpatConst -> Term.eq_constr_nounivs u.up_f f + | KpatFixed -> Term.eq_constr_nounivs u.up_f f | KpatEvar k -> isEvar_k k f | KpatLet -> isLetIn f | KpatLam -> isLambda f |