From cd1bb55339040bc272a9a752703e259e27ddbcd4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 10 May 2020 22:54:32 +0200
Subject: 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.
---
 test-suite/bugs/closed/bug_12234.v | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_12234.v

(limited to 'test-suite/bugs')

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.
-- 
cgit v1.2.3