From a7dc35f89f9a60233123acabc02956cc88a4ef88 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 10 Jun 2018 11:35:50 +0200 Subject: Fixes #7712 (an anomaly in reporting bad recursive notation format). --- test-suite/bugs/closed/7712.v | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 test-suite/bugs/closed/7712.v (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/7712.v b/test-suite/bugs/closed/7712.v new file mode 100644 index 000000000..a4e9697fa --- /dev/null +++ b/test-suite/bugs/closed/7712.v @@ -0,0 +1,4 @@ +(* This used to raise an anomaly *) + +Fail Reserved Notation "'[tele_arg' x ';' .. ';' z ]" + (format "[tele_arg '[hv' x .. z ']' ]"). -- cgit v1.2.3