diff options
| author | Enrico Tassi | 2018-09-19 16:58:36 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-09-19 16:58:36 +0200 |
| commit | ff74451389c13828c644157c960c0d314b389b95 (patch) | |
| tree | 224aa1c771c64984357702f244a13494b77cf569 | |
| parent | 007c084e3935eae639bb83c9dd9deefc1363d71d (diff) | |
[ssr] use the right environment in ssrpattern (fix #8454)
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 2 | ||||
| -rw-r--r-- | test-suite/ssr/ssrpattern.v | 7 |
2 files changed, 8 insertions, 1 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 20ea8b3667..aadb4fe5f6 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -1366,7 +1366,7 @@ let ssrpatterntac _ist arg gl = let concl0 = pf_concl gl in let concl0 = EConstr.Unsafe.to_constr concl0 in let (t, uc), concl_x = - fill_occ_pattern (Global.env()) sigma0 concl0 pat noindex 1 in + fill_occ_pattern (pf_env gl) sigma0 concl0 pat noindex 1 in let t = EConstr.of_constr t in let concl_x = EConstr.of_constr concl_x in let gl, tty = pf_type_of gl t in diff --git a/test-suite/ssr/ssrpattern.v b/test-suite/ssr/ssrpattern.v new file mode 100644 index 0000000000..422bb95fdf --- /dev/null +++ b/test-suite/ssr/ssrpattern.v @@ -0,0 +1,7 @@ +Require Import ssrmatching. + +Goal forall n, match n with 0 => 0 | _ => 0 end = 0. +Proof. + intro n. + ssrpattern (match _ with 0 => _ | S n' => _ end). +Abort. |