diff options
| author | Maxime Dénès | 2017-09-22 11:27:12 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-09-22 11:27:12 +0200 |
| commit | 95305e675a4e21f2425f2ffa9662095d864d9083 (patch) | |
| tree | b1e7804aa956ed5684754b43d8c66243376f9240 /test-suite | |
| parent | 7c760b08d690922fd15c489dd63a7be534d765ab (diff) | |
| parent | dc5b8f1793c6f7104f0b4762d9887be255709ead (diff) | |
Merge PR #1074: Fix BZ#5750 (recovering ability to print the hole of a context obtained by ltac pattern-matching)
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/5750.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5750.v b/test-suite/bugs/closed/5750.v new file mode 100644 index 0000000000..6d0e21f5d0 --- /dev/null +++ b/test-suite/bugs/closed/5750.v @@ -0,0 +1,3 @@ +(* Check printability of the hole of the context *) +Goal 0 = 0. +match goal with |- context c [0] => idtac c end. |