From 4009146b3b2445070c3f0551306bd701617ea280 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 12 Jul 2016 10:48:15 +0200
Subject: A short test on printing evars in Show Proof (this was wrong at some
 time).

---
 test-suite/output/ShowProof.out | 1 +
 test-suite/output/ShowProof.v   | 6 ++++++
 2 files changed, 7 insertions(+)
 create mode 100644 test-suite/output/ShowProof.out
 create mode 100644 test-suite/output/ShowProof.v

diff --git a/test-suite/output/ShowProof.out b/test-suite/output/ShowProof.out
new file mode 100644
index 0000000000..2d4be8bce7
--- /dev/null
+++ b/test-suite/output/ShowProof.out
@@ -0,0 +1 @@
+(fun x : Type => conj I ?Goal)
diff --git a/test-suite/output/ShowProof.v b/test-suite/output/ShowProof.v
new file mode 100644
index 0000000000..73ecaf2200
--- /dev/null
+++ b/test-suite/output/ShowProof.v
@@ -0,0 +1,6 @@
+(* Was #4524 *)
+Definition foo (x : Type) : True /\ True.
+Proof.
+split.
+- exact I.
+  Show Proof. (* Was not finding an evar name at some time *)
-- 
cgit v1.2.3