diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-12 10:48:15 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-12 14:30:03 +0200 |
| commit | 4009146b3b2445070c3f0551306bd701617ea280 (patch) | |
| tree | deea0512cd0de4b8e092c56f0e9b6c874b829f1a | |
| parent | 45207f8ed6c2484d1fe47576571e255570146e24 (diff) | |
A short test on printing evars in Show Proof (this was wrong at some time).
| -rw-r--r-- | test-suite/output/ShowProof.out | 1 | ||||
| -rw-r--r-- | test-suite/output/ShowProof.v | 6 |
2 files changed, 7 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) diff --git a/test-suite/output/ShowProof.v b/test-suite/output/ShowProof.v new file mode 100644 index 000000000..73ecaf220 --- /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 *) |