diff options
| author | Maxime Dénès | 2018-06-22 17:19:08 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-06-22 17:19:08 +0200 |
| commit | 01ceae32811c6d6450e40115384d68552444a000 (patch) | |
| tree | a4c863925a62af37dbcf6fbef502767216917ca8 /plugins/ssrmatching | |
| parent | df35025b2be4a0dc9aadecc0e3110a21012683cf (diff) | |
| parent | cb81adb6a438fe218e11192b09e085770c7d3067 (diff) | |
Merge PR #7776: [ssr] Fix rewrite with universes
Diffstat (limited to 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index c20e415b43..9d9b1b2e8c 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -561,8 +561,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 equal u.up_f f -> na - | KpatFixed when equal u.up_f f -> na + | KpatConst when eq_constr_nounivs u.up_f f -> na + | KpatFixed when 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 @@ -582,8 +582,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 -> equal u.up_f f - | KpatFixed -> equal u.up_f f + | KpatConst -> eq_constr_nounivs u.up_f f + | KpatFixed -> eq_constr_nounivs u.up_f f | KpatEvar k -> isEvar_k k f | KpatLet -> isLetIn f | KpatLam -> isLambda f @@ -764,8 +764,8 @@ let mk_tpattern_matcher ?(all_instances=false) let match_let f = match kind f with | LetIn (_, v, _, b) -> unif_EQ env sigma pv v && unif_EQ env' sigma pb b | _ -> false in match_let - | KpatFixed -> equal u.up_f - | KpatConst -> equal u.up_f + | KpatFixed -> eq_constr_nounivs u.up_f + | KpatConst -> eq_constr_nounivs u.up_f | KpatLam -> fun c -> (match kind c with | Lambda _ -> unif_EQ env sigma u.up_f c |