diff options
| author | Hugo Herbelin | 2020-05-10 22:54:32 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-14 12:21:30 +0200 |
| commit | cd1bb55339040bc272a9a752703e259e27ddbcd4 (patch) | |
| tree | d7628e94b5364ee9678b5b6ba1793450e5e613cc /test-suite | |
| parent | 6f2b88649ec0c1e27befe7bcd2cdbec0ccee95d6 (diff) | |
Fixes #12234 (wrong environment for Show Proof).
We take the env of the current goal with the context replaced with
section variables. In practice, this is the global env, but, maybe,
one day, a goal state will have its own env.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_12234.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_12234.v b/test-suite/bugs/closed/bug_12234.v new file mode 100644 index 0000000000..b99c5d524e --- /dev/null +++ b/test-suite/bugs/closed/bug_12234.v @@ -0,0 +1,9 @@ +(* Checking a Show Proof bug *) +Section S. +Variable A:Prop. +Theorem thm (a:A) : True. +assert (b:=a). +clear A a b. +Show Proof. +Abort. +End S. |