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 /mathcomp | |
| 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.
Diffstat (limited to 'mathcomp')
| -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 |