From 6363875a682ffa36f1f80fa74314c0b68cb2f065 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 6 Oct 2019 14:33:35 +0200
Subject: More tolerant in format for recursive notations.

This is probably a bit overkill but users are tempted to experiment
it, so we accept that both ends of a recursive notation are surrounded
with boxes which contain printing hints.

The alternative would have been to forbid the ends of a recursive
notation to be in boxes, but strictly speaking it is a bit more
restricting, even if I don't see a realistic use of the general form.
---
 test-suite/output/Notations4.out |  8 ++++++++
 test-suite/output/Notations4.v   | 26 ++++++++++++++++++++++++++
 2 files changed, 34 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 799d310fa7..43f88f42a5 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -63,3 +63,11 @@ fun '{| |} => true
      : R -> bool
 b = a
      : Prop
+The command has indeed failed with message:
+The format is not the same on the right- and left-hand sides of the special token "..".
+The command has indeed failed with message:
+The format is not the same on the right- and left-hand sides of the special token "..".
+The command has indeed failed with message:
+The format is not the same on the right- and left-hand sides of the special token "..".
+The command has indeed failed with message:
+The format is not the same on the right- and left-hand sides of the special token "..".
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 26c7840a16..4de6ce19b4 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -158,3 +158,29 @@ Check b = a.
 End Test.
 
 End L.
+
+Module M.
+
+(* Accept boxes around the end variables of a recursive notation (if equal boxes) *)
+
+Notation " {@ T1 ; T2 ; .. ; Tn } " :=
+  (and T1 (and T2 .. (and Tn True)..))
+  (format "'[v' {@  '[' T1 ']'  ;  '//' '['  T2  ']'  ;  '//' ..  ;   '//' '['  Tn  ']'  } ']'").
+
+Fail Notation " {@ T1 ; T2 ; .. ; Tn } " :=
+  (and T1 (and T2 .. (and Tn True)..))
+  (format "'[v' {@  '[' T1 ']'  ;  '//' '['  T2  ']'  ;  '//' ..  ;   '//' '['  Tn   ']'  } ']'").
+
+Fail Notation " {@ T1 ; T2 ; .. ; Tn } " :=
+  (and T1 (and T2 .. (and Tn True)..))
+  (format "'[v' {@  '[' T1 ']'  ;  '//' '['  T2  ']'  ;  '//' ..  ;   '//' '[v'  Tn  ']'  } ']'").
+
+Fail Notation " {@ T1 ; T2 ; .. ; Tn } " :=
+  (and T1 (and T2 .. (and Tn True)..))
+  (format "'[v' {@  '[' T1 ']'  ;  '//' '['  T2  ']'  ;  '//' ..  ;   '//' '['   Tn  ']'  } ']'").
+
+Fail Notation " {@ T1 ; T2 ; .. ; Tn } " :=
+  (and T1 (and T2 .. (and Tn True)..))
+  (format "'[v' {@  '[' T1 ']'  ;  '//' '['  T2  ']'   ;  '//' ..  ;   '//' '['  Tn  ']'  } ']'").
+
+End M.
-- 
cgit v1.2.3