From 95400806e85aaea109740e8fa77c0edb9f8b7a09 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 21 Sep 2017 17:06:37 +0200
Subject: 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".
---
 test-suite/bugs/closed/5750.v | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 test-suite/bugs/closed/5750.v

(limited to 'test-suite')

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.
-- 
cgit v1.2.3