diff options
| author | Hugo Herbelin | 2017-09-21 17:06:37 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-09-21 17:54:37 +0200 |
| commit | 95400806e85aaea109740e8fa77c0edb9f8b7a09 (patch) | |
| tree | f61cc56a27fb3e9f210618129787eabf2af1f88e /test-suite | |
| parent | 7e4535d62c4f8abc6537206e7abc34f1bb0be69d (diff) | |
A possible fix to BZ#5750 (ability to print context of ltac subterm match).
The main fix is to use is_ident_soft. The rest of the commit is to
provide something a bit more appealing than "?M-1".
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. |