diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-14 17:38:55 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-14 17:38:55 +0100 |
| commit | 71662ab9b00ac657663e192d942a4ba7f241fd59 (patch) | |
| tree | 3b421d598ff38fc3490c82df9d562ac7ec1bed44 /plugins/ssr | |
| parent | 0de6c50cb895bce977db0d5c1b603940706ccd03 (diff) | |
| parent | d69e4f55757c9066b0ae600d14ef89de3c8eb07d (diff) | |
Merge PR #6116: ssr: fill_occ_pattern: return valid ustate even if no match (fix #6106)
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 047ca509b..8493dbdbb 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1159,6 +1159,7 @@ let pf_interp_gen_aux ist gl to_ind ((oclr, occ), t) = let (c, ucst), cl = try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr cl) pat occ 1 with NoMatch -> redex_of_pattern env pat, (EConstr.Unsafe.to_constr cl) in + let gl = pf_merge_uc ucst gl in let c = EConstr.of_constr c in let cl = EConstr.of_constr cl in let clr = interp_clr sigma (oclr, (tag_of_cpattern t, c)) in |