From 21bcc5f6fc8db1ccad16dea89f1705a799c1d090 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 27 Dec 2018 08:56:23 +0100
Subject: Notations: Enforce strong evaluation of cases_pattern_of_glob_constr.

This is because it can raise Not_found in depth and we need to catch
it at the right time.
---
 test-suite/success/Notations2.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index 1b33863e3b..2533a39cc4 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -154,3 +154,14 @@ Module M16.
   Print Grammar foo.
   Print Grammar foo2.
 End M16.
+
+(* Example showing the need for strong evaluation of
+   cases_pattern_of_glob_constr (this used to raise Not_found at some
+   time) *)
+
+Module M17.
+
+Notation "# x ## t & u" := ((fun x => (x,t)),(fun x => (x,u))) (at level 0, x pattern).
+Check fun y : nat => # (x,z) ## y & y.
+
+End M17.
-- 
cgit v1.2.3


From a8a26c87d52c30e5e5d1ba76f1920e8bc68bcd45 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 27 Dec 2018 12:44:36 +0100
Subject: Notations: Fixing a printing bug with patterns.

Parameters had to be removed in cases_pattern_of_glob_constr.
---
 test-suite/output/Notations4.out | 20 ++++++++++++++++++++
 test-suite/output/Notations4.v   |  9 +++++++++
 2 files changed, 29 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index efa895d709..5bf4ec7bfb 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -53,3 +53,23 @@ Notation Cn := Foo.FooCn
 Expands to: Notation Notations4.J.Mfoo.Foo.Bar.Cn
 let v := 0%test17 in v : myint63
      : myint63
+fun y : nat => # (x, z) |-> y & y
+     : forall y : nat,
+       (?T1 * ?T2 -> ?T1 * ?T2 * nat) * (?T * ?T0 -> ?T * ?T0 * nat)
+where
+?T : [y : nat  pat : ?T * ?T0  p0 : ?T * ?T0  p := p0 : ?T * ?T0
+     |- Type] (pat, p0, p cannot be used)
+?T0 : [y : nat  pat : ?T * ?T0  p0 : ?T * ?T0  p := p0 : ?T * ?T0
+      |- Type] (pat, p0, p cannot be used)
+?T1 : [y : nat  pat : ?T1 * ?T2  p0 : ?T1 * ?T2  p := p0 : ?T1 * ?T2
+      |- Type] (pat, p0, p cannot be used)
+?T2 : [y : nat  pat : ?T1 * ?T2  p0 : ?T1 * ?T2  p := p0 : ?T1 * ?T2
+      |- Type] (pat, p0, p cannot be used)
+fun y : nat => # (x, z) |-> (x + y) & (y + z)
+     : forall y : nat,
+       (nat * ?T -> nat * ?T * nat) * (?T0 * nat -> ?T0 * nat * nat)
+where
+?T : [y : nat  pat : nat * ?T  p0 : nat * ?T  p := p0 : nat * ?T
+     |- Type] (pat, p0, p cannot be used)
+?T0 : [y : nat  pat : ?T0 * nat  p0 : ?T0 * nat  p := p0 : ?T0 * nat
+      |- Type] (pat, p0, p cannot be used)
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index b4c65ce196..b33ad17ed4 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -210,3 +210,12 @@ Module NumeralNotations.
     Check let v := 0%test17 in v : myint63.
   End Test17.
 End NumeralNotations.
+
+Module K.
+
+Notation "# x |-> t & u" := ((fun x => (x,t)),(fun x => (x,u)))
+  (at level 0, x pattern, t, u at level 39).
+Check fun y : nat => # (x,z) |-> y & y.
+Check fun y : nat => # (x,z) |-> (x + y) & (y + z).
+
+End K.
-- 
cgit v1.2.3