aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/ShowProof.out
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-07-12 10:48:15 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-07-12 14:30:03 +0200
commit4009146b3b2445070c3f0551306bd701617ea280 (patch)
treedeea0512cd0de4b8e092c56f0e9b6c874b829f1a /test-suite/output/ShowProof.out
parent45207f8ed6c2484d1fe47576571e255570146e24 (diff)
A short test on printing evars in Show Proof (this was wrong at some time).
Diffstat (limited to 'test-suite/output/ShowProof.out')
-rw-r--r--test-suite/output/ShowProof.out1
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/output/ShowProof.out b/test-suite/output/ShowProof.out
new file mode 100644
index 000000000..2d4be8bce
--- /dev/null
+++ b/test-suite/output/ShowProof.out
@@ -0,0 +1 @@
+(fun x : Type => conj I ?Goal)