From 94bdd90bacc4d4a92b79bbe0db532e523fbcbce8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 4 Nov 2016 17:03:04 +0100
Subject: Test for #4966 ("auto" wrongly seen as "auto with *" when in position
 of ident).

---
 test-suite/bugs/closed/4966.v | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 test-suite/bugs/closed/4966.v

diff --git a/test-suite/bugs/closed/4966.v b/test-suite/bugs/closed/4966.v
new file mode 100644
index 0000000000..bd93cdc858
--- /dev/null
+++ b/test-suite/bugs/closed/4966.v
@@ -0,0 +1,10 @@
+(* Interpretation of auto as an argument of an ltac function (i.e. as an ident) was wrongly "auto with *" *)
+
+Axiom proof_admitted : False.
+Hint Extern 0 => case proof_admitted : unused.
+Ltac do_tac tac := tac.
+
+Goal False.
+  Set Ltac Profiling.
+  Fail solve [ do_tac auto ].
+Abort.
-- 
cgit v1.2.3