diff options
| author | Pierre-Marie Pédrot | 2020-05-22 12:02:49 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-22 12:02:49 +0200 |
| commit | ea9463bc10e83759586a41d562e996e1d34e627f (patch) | |
| tree | 010948179bddaa470ac6686c2dc8192171909723 /plugins | |
| parent | 7e09ee64b721baf0803c5fdb91c4687fded112cb (diff) | |
| parent | 30ccbef77b0a5c1545018434c397344324ba5f4a (diff) | |
Merge PR #12295: Fixes #12233: printing environment corrupted with eta-expansion of "match" branches
Reviewed-by: gares
Ack-by: ppedrot
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index e004613ef3..5d6e7c51d0 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -370,6 +370,11 @@ let ehole_var = EConstr.mkVar (Id.of_string "_") let pr_econstr_pat env sigma c0 = let rec wipe_evar c = let open EConstr in if isEvar sigma c then ehole_var else map sigma wipe_evar c in + let dummy_decl = + let dummy_prod = mkProd (make_annot Anonymous Sorts.Relevant,mkProp,mkProp) in + let na = make_annot (EConstr.destVar sigma ehole_var) Sorts.Relevant in + Context.Named.Declaration.(LocalAssum (na, dummy_prod)) in + let env = Environ.push_named dummy_decl env in pr_econstr_env env sigma (wipe_evar c0) (* Turn (new) evars into metas *) |