From 65505b835d6a77b8702d11d09e8cf6b84c529c65 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 12 Aug 2017 13:42:01 +0200
Subject: Adding support for re-folding notation referring to isolated "forall
 '(x,y), t".

Was apparently forgotten in a67bd7f9.
---
 test-suite/output/Notations3.out | 2 ++
 test-suite/output/Notations3.v   | 5 +++++
 2 files changed, 7 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 1b57252752..bd24f3f616 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -138,3 +138,5 @@ amatch = mmatch 0 (with 0 => 1| 1 => 2 end)
      : unit
 alist = [0; 1; 2]
      : list nat
+! '{{x, y}}, x + y = 0
+     : Prop
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index a8d6c97fbd..773241f90e 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -253,3 +253,8 @@ Definition alist := [0;1;2].
 Print alist.
 
 End B.
+
+(* Test contraction of "forall x, let 'pat := x in ..." into "forall 'pat, ..." *)
+(* for isolated "forall" (was not working already in 8.6) *)
+Notation "! x .. y , A" := (id (forall x, .. (id (forall y, A)) .. )) (at level 200, x binder).
+Check ! '(x,y), x+y=0.
-- 
cgit v1.2.3


From 66eae7fa7f8e1f075a8c84afad48af4d35c4bfaf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 22 Nov 2017 05:32:17 +0100
Subject: Notations: Do not consider a non-occurring variable as a binder-only
 variable.

---
 test-suite/success/Notations2.v | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index 2655b651a0..08d904cea0 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -92,8 +92,7 @@ Check ##### 0 _ 0%bool 0%bool : prod' bool bool.
 Check fun A (x :prod' bool A) => match x with ##### 0 _ y 0%bool => 2 | _ => 1 end.
 
 (* 10. Check computation of binding variable through other notations *)
-(* i should be detected as binding variable and the scopes not being checked *)
-
+(* it should be detected as binding variable and the scopes not being checked *)
 Notation "'FUNNAT' i => t" := (fun i : nat => i = t) (at level 200).
 Notation "'Funnat' i => t" := (FUNNAT i => t + i%nat) (at level 200).
 
@@ -105,3 +104,10 @@ Notation "[:: x1 ; .. ; xn ]" := (cons x1 .. (cons xn nil) ..).
 Check [:: 1 ; 2 ; 3 ].
 Check [:: 1 ; 2 ; 3 & nil ]. (* was failing *)
 End A.
+
+(* 12. Preventively check that a variable which does not occur can be instantiated *)
+(* by any term. In particular, it should not be restricted to a binder *)
+Module M12.
+Notation "N ++ x" := (S x) (only parsing).
+Check 2 ++ 0.
+End M12.
-- 
cgit v1.2.3


From 6b9a9124d3bd24fe9305df613547139f6f609c60 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 10 Aug 2017 16:15:57 +0200
Subject: Moving the argument of CProdN/CLambdaN from binder_expr to
 local_binder_expr.

The motivations are:

- To reflect the concrete syntax more closely.
- To factorize the different places where "contexts" are internalized:
  before this patch, there is a different treatment of `Definition f
  '(x,y) := x+y` and `Definition f := fun '(x,y) => x+y`, and a hack
  to interpret `Definition f `pat := c : t`. With the patch, the fix
  to avoid seeing a variable named `pat` works for both `fun 'x =>
  ...` and `Definition f 'x := ...`.

The drawbacks are:

- Counterpart to reflecting the concrete syntax more closerly, there
  are more redundancies in the syntax. For instance, the case `CLetIn
  (na,b,t,c)` can appears also in the form `CProdN (CLocalDef
  (na,b,t)::rest,d)` and `CLambdaN (CLocalDef (na,b,t)::rest,d)`.
- Changes in the API, hence adaptation of plugins referring to `constr_expr` needed.
---
 test-suite/output/PatternsInBinders.out | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
index 95be04c32c..6b09c33084 100644
--- a/test-suite/output/PatternsInBinders.out
+++ b/test-suite/output/PatternsInBinders.out
@@ -31,7 +31,7 @@ exists '(x, y) '(z, w), swap (x, y) = (z, w)
      : Prop
 both_z = 
 fun pat : nat * nat =>
-let '(n, p) as pat0 := pat return (F pat0) in (Z n, Z p) : F (n, p)
+let '(n, p) as x := pat return (F x) in (Z n, Z p) : F (n, p)
      : forall pat : nat * nat, F pat
 fun '(x, y) '(z, t) => swap (x, y) = (z, t)
      : A * B -> B * A -> Prop
-- 
cgit v1.2.3


From 9324dcf528f16be420b08c376a6580c8987f50fd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 10 Aug 2017 17:10:48 +0200
Subject: Using name given by user to name a 'pat, if any.

This works for contexts in Definition and co, but not yet for "fun" and co.
---
 test-suite/output/PatternsInBinders.out | 6 ++++++
 test-suite/output/PatternsInBinders.v   | 5 +++++
 2 files changed, 11 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
index 6b09c33084..8a6d94c732 100644
--- a/test-suite/output/PatternsInBinders.out
+++ b/test-suite/output/PatternsInBinders.out
@@ -39,3 +39,9 @@ forall '(x, y) '(z, t), swap (x, y) = (z, t)
      : Prop
 fun (pat : nat) '(x, y) => x + y = pat
      : nat -> nat * nat -> Prop
+f = fun x : nat => x + x
+     : nat -> nat
+
+Argument scope is [nat_scope]
+fun x : nat => x + x
+     : nat -> nat
diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v
index 0bad472f41..d671053c07 100644
--- a/test-suite/output/PatternsInBinders.v
+++ b/test-suite/output/PatternsInBinders.v
@@ -67,3 +67,8 @@ End Suboptimal.
 
 (** Test risk of collision for internal name *)
 Check fun pat => fun '(x,y) => x+y = pat.
+
+(** Test name in degenerate case *)
+Definition f 'x := x+x.
+Print f.
+Check fun 'x => x+x.
-- 
cgit v1.2.3


From 7c10b4020e061fb14e01cb3abc92bb5265aa65b9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 13 Aug 2017 18:17:32 +0200
Subject: Fixing/improving notations with recursive patterns.

- The "terminator" of a recursive notation is now interpreted in the
  environment in which it occurs rather than the environment at the
  beginning of the recursive patterns.

  Note that due to a tolerance in checking unbound variables of
  notations, a variable unbound in the environment was still working
  ok as long as no user-given variable was shadowing a private
  variable of the notation - see the "exists_mixed" example in
  test-suite.

  Conversely, in a notation such as:

    Notation "!! x .. y # A #" :=
      ((forall x, True), .. ((forall y, True), A) ..)
      (at level 200, x binder).
    Check !! a b # a=b #.

  The unbound "a" was detected only at pretyping and not as expected
  at internalizing time, due to "a=b" interpreted in context
  containing a and b.

- Similarly, each binder is now interpreted in the environment in
  which it occurs rather than as if the sequence of binders was
  dependent from the left to the right (such a dependency was ok for
  "forall" or "exists" but not in general).

  For instance, in:

    Notation "!! x .. y # A #" :=
      ((forall x, True), .. ((forall y, True), A) ..)
      (at level 200, x binder).
    Check !! (a:nat) (b:a=a) # True #.

  The illegal dependency of the type of b in a was detected only at
  pretyping time.

- If a let-in occurs in the sequence of binders of a notation with a
  recursive pattern, it is now inserted in between the occurrences of
  the iterator rather than glued with the forall/fun of the iterator.
  For instance, in:

    Notation "'exists_true' x .. y , P" :=
      (exists x, True /\ .. (exists y, True /\ P) ..)
      (at level 200, x binder).
    Check exists_true '(x,y) (u:=0), x=y.

  We now get

    exists '(x, y), True /\ (let u := 0 in True /\ x = y)

  while we had before the let-in breaking the repeated pattern:

    exists '(x, y), (let u := 0 in True /\ x = y)

  This is more compositional, and, in particular, the printer algorithm
  now recognizes the pattern which is otherwise broken.
---
 test-suite/output/Notations3.out | 21 +++++++++++++++++++++
 test-suite/output/Notations3.v   | 20 ++++++++++++++++++++
 2 files changed, 41 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index bd24f3f616..cf69874ca7 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -140,3 +140,24 @@ alist = [0; 1; 2]
      : list nat
 ! '{{x, y}}, x + y = 0
      : Prop
+exists x : nat,
+  nat ->
+  exists y : nat,
+    nat ->
+    exists '{{u, t}}, forall z1 : nat, z1 = 0 /\ x + y = 0 /\ u + t = 0
+     : Prop
+exists x : nat,
+  nat ->
+  exists y : nat,
+    nat ->
+    exists '{{z, t}}, forall z2 : nat, z2 = 0 /\ x + y = 0 /\ z + t = 0
+     : Prop
+exists_true '{{x, y}},
+(let u := 0 in exists_true '{{z, t}}, x + y = 0 /\ z + t = 0)
+     : Prop
+exists_true (A : Type) (R : A -> A -> Prop) (_ : Reflexive R),
+(forall x : A, R x x)
+     : Prop
+exists_true (x : nat) (A : Type) (R : A -> A -> Prop) 
+(_ : Reflexive R) (y : nat), x + y = 0 -> forall z : A, R z z
+     : Prop
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 773241f90e..3e07fbce91 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -258,3 +258,23 @@ End B.
 (* for isolated "forall" (was not working already in 8.6) *)
 Notation "! x .. y , A" := (id (forall x, .. (id (forall y, A)) .. )) (at level 200, x binder).
 Check ! '(x,y), x+y=0.
+
+(* Check that the terminator of a recursive pattern is interpreted in
+   the correct environment of bindings *)
+Notation "'exists_mixed' x .. y , P" := (ex (fun x => forall z:nat, .. (ex (fun y => forall z:nat, z=0 /\ P)) ..)) (at level 200, x binder).
+Check exists_mixed x y '(u,t), x+y=0/\u+t=0.
+Check exists_mixed x y '(z,t), x+y=0/\z+t=0.
+
+(* Check that intermediary let-in are inserted inbetween instances of
+   the repeated pattern *)
+Notation "'exists_true' x .. y , P" := (exists x, True /\ .. (exists y, True /\ P) ..) (at level 200, x binder).
+Check exists_true '(x,y) (u:=0) '(z,t), x+y=0/\z+t=0.
+
+(* Check that generalized binders are correctly interpreted *)
+
+Module G.
+Generalizable Variables A R.
+Class Reflexive {A:Type} (R : A->A->Prop) := reflexivity : forall x : A, R x x.
+Check exists_true `{Reflexive A R}, forall x, R x x.
+Check exists_true x `{Reflexive A R} y, x+y=0 -> forall z, R z z.
+End G.
-- 
cgit v1.2.3


From d4c2ed95fcfd64cdcc10e51e40be739d9f1c4a74 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 13 Aug 2017 20:05:03 +0200
Subject: Allows recursive patterns for binders to be associative on the left.

This makes treatment of recursive binders closer to the one of
recursive terms. It is unclear whether there are interesting notations
liable to use this, but this shall make easier mixing recursive
binders and recursive terms as in next commits.

Example of (artificial) notation that this commit supports:

  Notation "! x .. y # A #" :=
    (.. (A,(forall x, True)) ..,(forall y, True))
    (at level 200, x binder).
---
 test-suite/output/Notations3.out | 2 ++
 test-suite/output/Notations3.v   | 4 ++++
 2 files changed, 6 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index cf69874ca7..e114ea8948 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -161,3 +161,5 @@ exists_true (A : Type) (R : A -> A -> Prop) (_ : Reflexive R),
 exists_true (x : nat) (A : Type) (R : A -> A -> Prop) 
 (_ : Reflexive R) (y : nat), x + y = 0 -> forall z : A, R z z
      : Prop
+{{{{True, nat -> True}}, nat -> True}}
+     : Prop * Prop * Prop
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 3e07fbce91..a7fed35611 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -278,3 +278,7 @@ Class Reflexive {A:Type} (R : A->A->Prop) := reflexivity : forall x : A, R x x.
 Check exists_true `{Reflexive A R}, forall x, R x x.
 Check exists_true x `{Reflexive A R} y, x+y=0 -> forall z, R z z.
 End G.
+
+(* Allows recursive patterns for binders to be associative on the left *)
+Notation "!! x .. y # A #" := (.. (A,(forall x, True)) ..,(forall y, True)) (at level 200, x binder).
+Check !! a b : nat # True #.
-- 
cgit v1.2.3


From a18e87f6a929ce296f8c277b310e286151e06293 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 14 Aug 2017 01:27:04 +0200
Subject: Allowing variables used in recursive notation to occur several times
 in pattern.

This allows for instance to support recursive notations of the form:

Notation "! x .. y # A #" :=
  (((forall x, x=x),(forall x, x=0)), .. (((forall y, y=y),(forall y, y=0)), A) ..)
  (at level 200, x binder).
---
 test-suite/output/Notations3.out | 10 ++++++++++
 test-suite/output/Notations3.v   | 25 +++++++++++++++++++++++++
 2 files changed, 35 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index e114ea8948..5bfdec9898 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -163,3 +163,13 @@ exists_true (x : nat) (A : Type) (R : A -> A -> Prop)
      : Prop
 {{{{True, nat -> True}}, nat -> True}}
      : Prop * Prop * Prop
+{{D 1, 2}}
+     : nat * nat * (nat * nat * (nat * nat))
+! a b : nat # True #
+     : Prop * (Prop * Prop)
+!!!! a b : nat # True #
+     : Prop * Prop * (Prop * Prop * Prop)
+@@ a b : nat # a = b # b = a #
+     : Prop * Prop
+exists_non_null x y z t : nat , x = y /\ z = t
+     : Prop
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index a7fed35611..c7e32f733a 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -282,3 +282,28 @@ End G.
 (* Allows recursive patterns for binders to be associative on the left *)
 Notation "!! x .. y # A #" := (.. (A,(forall x, True)) ..,(forall y, True)) (at level 200, x binder).
 Check !! a b : nat # True #.
+
+(* Examples where the recursive pattern refer several times to the recursive variable *)
+
+Notation "{{D  x , .. , y }}" := ((x,x), .. ((y,y),(0,0)) ..).
+Check {{D 1, 2 }}.
+
+Notation "! x .. y # A #" :=
+  ((forall x, x=x), .. ((forall y, y=y), A) ..)
+  (at level 200, x binder).
+Check ! a b : nat # True #.
+
+Notation "!!!! x .. y # A #" :=
+  (((forall x, x=x),(forall x, x=0)), .. (((forall y, y=y),(forall y, y=0)), A) ..)
+  (at level 200, x binder).
+Check !!!! a b : nat # True #.
+
+Notation "@@ x .. y # A # B #" :=
+  ((forall x, .. (forall y, A) ..), (forall x, .. (forall y, B) ..))
+  (at level 200, x binder).
+Check @@ a b : nat # a=b # b=a #.
+
+Notation "'exists_non_null' x .. y  , P" :=
+  (ex (fun x => x <> 0 /\ .. (ex (fun y => y <> 0 /\ P)) ..))
+  (at level 200, x binder).
+Check exists_non_null x y z t , x=y/\z=t.
-- 
cgit v1.2.3


From 96d6ef7036e19bf1def1512abae5ef8c6ace06b0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 14 Aug 2017 13:29:39 +0200
Subject: Supporting recursive notations reversing the left-to-right order.

Seizing this opportunity to generalize the possibility for different
associativity into simply reversing the order or not. Also dropping
some dead code.

Example of recursive notation now working:

  Notation "[ a , .. , b |- A ]" := (cons b .. (cons a nil) .., A).
---
 test-suite/output/Notations.out  |  2 +-
 test-suite/output/Notations3.out | 18 ++++++++++++++++++
 test-suite/output/Notations3.v   | 19 +++++++++++++++++++
 3 files changed, 38 insertions(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 2f0ee765db..891296b0a1 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -41,7 +41,7 @@ fun x : nat => ifn x is succ n then n else 0
 -4
      : Z
 The command has indeed failed with message:
-x should not be bound in a recursive pattern of the right-hand side.
+Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
 in the right-hand side, y and z should appear in
 term position as part of a recursive pattern.
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 5bfdec9898..58dabe51e5 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -173,3 +173,21 @@ exists_true (x : nat) (A : Type) (R : A -> A -> Prop)
      : Prop * Prop
 exists_non_null x y z t : nat , x = y /\ z = t
      : Prop
+{{RL 1, 2}}
+     : nat * (nat * nat)
+{{RR 1, 2}}
+     : nat * nat * nat
+@pair nat (prod nat nat) (S (S O)) (@pair nat nat (S O) O)
+     : prod nat (prod nat nat)
+@pair (prod nat nat) nat (@pair nat nat O (S (S O))) (S O)
+     : prod (prod nat nat) nat
+{{RLRR 1, 2}}
+     : nat * (nat * nat) * (nat * nat * nat) * (nat * (nat * nat)) *
+       (nat * nat * nat)
+pair
+  (pair
+     (pair (pair (S (S O)) (pair (S O) O)) (pair (pair O (S (S O))) (S O)))
+     (pair (S O) (pair (S (S O)) O))) (pair (pair O (S O)) (S (S O)))
+     : prod
+         (prod (prod (prod nat (prod nat nat)) (prod (prod nat nat) nat))
+            (prod nat (prod nat nat))) (prod (prod nat nat) nat)
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index c7e32f733a..fd5846e71c 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -307,3 +307,22 @@ Notation "'exists_non_null' x .. y  , P" :=
   (ex (fun x => x <> 0 /\ .. (ex (fun y => y <> 0 /\ P)) ..))
   (at level 200, x binder).
 Check exists_non_null x y z t , x=y/\z=t.
+
+(* Examples where the recursive pattern is in reverse order *)
+
+Notation "{{RL  c , .. , d }}" := (pair d .. (pair c 0) ..).
+Check {{RL 1 , 2}}.
+
+Notation "{{RR  c , .. , d }}" := (pair .. (pair 0 d) .. c).
+Check {{RR 1 , 2}}.
+
+Set Printing All.
+Check {{RL 1 , 2}}.
+Check {{RR 1 , 2}}.
+Unset Printing All.
+
+Notation "{{RLRR  c , .. , d }}" := (pair d .. (pair c 0) .., pair .. (pair 0 d) .. c, pair c .. (pair d 0) .., pair .. (pair 0 c) .. d).
+Check {{RLRR 1 , 2}}.
+Unset Printing Notations.
+Check {{RLRR 1 , 2}}.
+Set Printing Notations.
-- 
cgit v1.2.3


From 34cf92821e03a2c6ce64c78c66a00624d0fe9c99 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 15 Aug 2017 14:55:44 +0200
Subject: In printing notations with "match", reasoning up to the order of
 clauses.

---
 test-suite/output/Notations3.out | 2 ++
 test-suite/output/Notations3.v   | 7 +++++++
 2 files changed, 9 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 58dabe51e5..9c711ff265 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -191,3 +191,5 @@ pair
      : prod
          (prod (prod (prod nat (prod nat nat)) (prod (prod nat nat) nat))
             (prod nat (prod nat nat))) (prod (prod nat nat) nat)
+fun x : nat => if x is n .+ 1 then n else 1
+     : nat -> nat
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index fd5846e71c..d81cc702af 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -326,3 +326,10 @@ Check {{RLRR 1 , 2}}.
 Unset Printing Notations.
 Check {{RLRR 1 , 2}}.
 Set Printing Notations.
+
+(* Check insensitivity of "match" clauses to order *)
+
+Notation "'if' t 'is' n .+ 1 'then' p 'else' q" :=
+  (match t with S n => p | 0 => q end)
+  (at level 200).
+Check fun x => if x is n.+1 then n else 1.
-- 
cgit v1.2.3


From 398358618bb3eabfe822b79c669703c1c33b67e6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 15 Aug 2017 18:32:02 +0200
Subject: Adding patterns in the category of binders for notations.

For instance, the following is now possible:

  Check {(x,y)|x+y=0}.

Some questions remains. Maybe, by consistency, the notation should be
"{'(x,y)|x+y=0}"...
---
 test-suite/output/Notations3.out | 2 ++
 test-suite/output/Notations3.v   | 4 ++++
 2 files changed, 6 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 9c711ff265..5bb77b8fde 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -193,3 +193,5 @@ pair
             (prod nat (prod nat nat))) (prod (prod nat nat) nat)
 fun x : nat => if x is n .+ 1 then n else 1
      : nat -> nat
+{{{x, y}} : nat * nat | x + y = 0}
+     : Set
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index d81cc702af..201198b3eb 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -333,3 +333,7 @@ Notation "'if' t 'is' n .+ 1 'then' p 'else' q" :=
   (match t with S n => p | 0 => q end)
   (at level 200).
 Check fun x => if x is n.+1 then n else 1.
+
+(* Examples with binding patterns *)
+
+Check {(x,y)|x+y=0}.
-- 
cgit v1.2.3


From edd0d22429354a5f2c703a8c7bd1f775e2f97d9e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 12 Aug 2017 09:15:40 +0200
Subject: Adding support for parsing subterms of a notation as "pattern".

This allows in particular to define notations with 'pat style binders.

E.g.:

A non-trivial change in this commit is storing binders and patterns
separately from terms.

This is not strictly necessary but has some advantages.

However, it is relatively common to have binders also used as terms,
or binders parsed as terms. Thus, it is already relatively common to
embed binders into terms (see e.g. notation for ETA in output test
Notations3.v) or to coerce terms to idents (see e.g. the notation for
{x|P} where x is parsed as a constr).

So, it is as simple to always store idents (and eventually patterns)
as terms.
---
 test-suite/output/Notations3.out | 2 ++
 test-suite/output/Notations3.v   | 7 +++++++
 2 files changed, 9 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 5bb77b8fde..fb2d375c27 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -195,3 +195,5 @@ fun x : nat => if x is n .+ 1 then n else 1
      : nat -> nat
 {{{x, y}} : nat * nat | x + y = 0}
      : Set
+exists2' {{x, y}}, x = 0 & y = 0
+     : Prop
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 201198b3eb..46e0c1b1b5 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -337,3 +337,10 @@ Check fun x => if x is n.+1 then n else 1.
 (* Examples with binding patterns *)
 
 Check {(x,y)|x+y=0}.
+
+Notation "'exists2'' x , p & q" := (ex2 (fun x => p) (fun x => q))
+  (at level 200, x pattern, p at level 200, right associativity,
+    format "'[' 'exists2''  '/  ' x ,  '/  ' '[' p  &  '/' q ']' ']'")
+  : type_scope.
+
+Check exists2' (x,y), x=0 & y=0.
-- 
cgit v1.2.3


From 3a6b1d2c04ceeb568accbc9ddfc3fc0f14faf25b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 17 Aug 2017 12:35:56 +0200
Subject: Respecting the ident/pattern distinction in notation modifiers.

---
 test-suite/output/Notations3.out | 3 +++
 test-suite/output/Notations3.v   | 7 +++++++
 2 files changed, 10 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index fb2d375c27..7c47c0885d 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -197,3 +197,6 @@ fun x : nat => if x is n .+ 1 then n else 1
      : Set
 exists2' {{x, y}}, x = 0 & y = 0
      : Prop
+exists2 x : nat * nat,
+  let '{{y, z}} := x in y > z & let '{{y, z}} := x in z > y
+     : Prop
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 46e0c1b1b5..ee6f0a09e0 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -338,9 +338,16 @@ Check fun x => if x is n.+1 then n else 1.
 
 Check {(x,y)|x+y=0}.
 
+Module D.
 Notation "'exists2'' x , p & q" := (ex2 (fun x => p) (fun x => q))
   (at level 200, x pattern, p at level 200, right associativity,
     format "'[' 'exists2''  '/  ' x ,  '/  ' '[' p  &  '/' q ']' ']'")
   : type_scope.
 
 Check exists2' (x,y), x=0 & y=0.
+End D.
+
+(* Ensuring for reparsability that printer of notations does not use a
+   pattern where only an ident could be reparsed *)
+
+Check ex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y).
-- 
cgit v1.2.3


From bc73f267ad2da0f1e24e66cb481725be018a8ce6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 21 Aug 2017 23:25:21 +0200
Subject: A (significant) simplification in printing notations with recursive
 binders.

For historical reasons (this was one of the first examples of
notations with binders), there was a special treatment for notations
whose right-hand side had the form "forall x, P" or "fun x => P". Not
only this is not necessary, but this prevents notations binding to
expressions such as "forall x, x>0 -> P" to be used in printing.

We let the general case absorb this particular case.

We add the integration of "let x:=c in ..." in the middle of a
notation with recursive binders as part of the binder list, reprinting
it "(x:=c)" (this was formerly the case only for the above particular
case).

Note that integrating "let" in sequence of binders is stil not the
case for the regular "forall"/"fun". Should we?
---
 test-suite/output/Notations2.out | 6 ++----
 test-suite/output/Notations2.v   | 5 +++--
 test-suite/output/Notations3.out | 5 +++--
 test-suite/output/Notations3.v   | 5 +++++
 4 files changed, 13 insertions(+), 8 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 121a369a94..0e5f399036 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -17,10 +17,8 @@ fun (P : nat -> nat -> Prop) (x : nat) => exists y, P x y
 ∃ n p : nat, n + p = 0
      : Prop
 let a := 0 in
-∃ x y : nat,
-let b := 1 in
-let c := b in
-let d := 2 in ∃ z : nat, let e := 3 in let f := 4 in x + y = z + d
+∃ (x y : nat) (b := 1) (c := b) (d := 2) (z : nat) (e := 3) (f := 4), 
+x + y = z + d
      : Prop
 ∀ n p : nat, n + p = 0
      : Prop
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 531398bb0b..923caedace 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -36,8 +36,9 @@ Check fun P:nat->nat->Prop => fun x:nat => ex (P x).
 
 (* Test notations with binders *)
 
-Notation "∃  x .. y , P":= (ex (fun x => .. (ex (fun y => P)) ..))
-  (x binder, y binder, at level 200, right associativity).
+Notation "∃ x .. y , P":= (ex (fun x => .. (ex (fun y => P)) ..))
+  (x binder, y binder, at level 200, right associativity,
+  format "'[  ' ∃  x  ..  y ']' ,  P").
 
 Check (∃ n p, n+p=0).
 
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 7c47c0885d..cb18fa3564 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -152,8 +152,7 @@ exists x : nat,
     nat ->
     exists '{{z, t}}, forall z2 : nat, z2 = 0 /\ x + y = 0 /\ z + t = 0
      : Prop
-exists_true '{{x, y}},
-(let u := 0 in exists_true '{{z, t}}, x + y = 0 /\ z + t = 0)
+exists_true '{{x, y}} (u := 0) '{{z, t}}, x + y = 0 /\ z + t = 0
      : Prop
 exists_true (A : Type) (R : A -> A -> Prop) (_ : Reflexive R),
 (forall x : A, R x x)
@@ -173,6 +172,8 @@ exists_true (x : nat) (A : Type) (R : A -> A -> Prop)
      : Prop * Prop
 exists_non_null x y z t : nat , x = y /\ z = t
      : Prop
+forall_non_null x y z t : nat , x = y /\ z = t
+     : Prop
 {{RL 1, 2}}
      : nat * (nat * nat)
 {{RR 1, 2}}
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index ee6f0a09e0..d768b9ba49 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -308,6 +308,11 @@ Notation "'exists_non_null' x .. y  , P" :=
   (at level 200, x binder).
 Check exists_non_null x y z t , x=y/\z=t.
 
+Notation "'forall_non_null' x .. y  , P" :=
+  (forall x, x <> 0 -> .. (forall y, y <> 0 -> P) ..)
+  (at level 200, x binder).
+Check forall_non_null x y z t , x=y/\z=t.
+
 (* Examples where the recursive pattern is in reverse order *)
 
 Notation "{{RL  c , .. , d }}" := (pair d .. (pair c 0) ..).
-- 
cgit v1.2.3


From 15abe33f55b317410223bd48576fa35c81943ff9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 14 Feb 2018 19:55:21 +0100
Subject: Refining the strategy for glueing let-ins to a sequence of binders.

To deal with existing notations starting with a "let" (see notation
"for" in output/Notation2.v) we adopt the pragmatic approach of
glueing only inner let by default.

Ideally, it might be nicer to detect if there is an overlap of
notation, and not to glue only in case of overlap. We could also
decide that a notation starting with a "let" should always be
protected by some constant, say "id", so as to avoid possible
collisions, but this would require changes user side.
---
 test-suite/output/Notations2.out | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 0e5f399036..6ffe56e11f 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -17,8 +17,9 @@ fun (P : nat -> nat -> Prop) (x : nat) => exists y, P x y
 ∃ n p : nat, n + p = 0
      : Prop
 let a := 0 in
-∃ (x y : nat) (b := 1) (c := b) (d := 2) (z : nat) (e := 3) (f := 4), 
-x + y = z + d
+∃ (x y : nat) (b := 1) (c := b) (d := 2) (z : nat), 
+let e := 3 in
+let f := 4 in x + y = z + d
      : Prop
 ∀ n p : nat, n + p = 0
      : Prop
-- 
cgit v1.2.3


From 50970e4043d73d9a4fbd17ffe765745f6d726317 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 21 Aug 2017 23:01:04 +0200
Subject: Using an "as" clause when needed for printing irrefutable patterns.

Example which is now reprinted as parsed:

  fun '((x,y) as z) => (y,x)=z
---
 test-suite/output/Notations3.out |  8 ++++++++
 test-suite/output/Notations3.v   | 20 ++++++++++++++++++++
 2 files changed, 28 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index cb18fa3564..0463e5bfbd 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -201,3 +201,11 @@ exists2' {{x, y}}, x = 0 & y = 0
 exists2 x : nat * nat,
   let '{{y, z}} := x in y > z & let '{{y, z}} := x in z > y
      : Prop
+fun '({{x, y}} as z) => x + y = 0 /\ z = z
+     : nat * nat -> Prop
+myexists ({{x, y}} as z), x + y = 0 /\ z = z
+     : Prop
+exists '({{x, y}} as z), x + y = 0 /\ z = z
+     : Prop
+∀ '({{x, y}} as z), x + y = 0 /\ z = z
+     : Prop
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index d768b9ba49..9ec459ed69 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -356,3 +356,23 @@ End D.
    pattern where only an ident could be reparsed *)
 
 Check ex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y).
+
+(* A canonical example of a notation with a non-recursive binder *)
+
+Parameter myex : forall {A}, (A -> Prop) -> Prop.
+Notation "'myexists' x , p" := (myex (fun x => p))
+  (at level 200, x pattern, p at level 200, right associativity).
+
+(* A canonical example of a notation with recursive binders *)
+
+Notation "∀  x .. y , P" := (forall x, .. (forall y, P) ..)
+  (at level 200, x binder, y binder, right associativity) : type_scope.
+
+(* Check that printing 'pat uses an "as" when the variable bound to
+   the pattern is dependent. We check it for the three kinds of
+   notations involving bindings of patterns *)
+
+Check fun '((x,y) as z) => x+y=0/\z=z.    (* Primitive fun/forall *)
+Check myexists ((x,y) as z), x+y=0/\z=z.  (* Isolated binding pattern *)
+Check exists '((x,y) as z), x+y=0/\z=z.   (* Applicative recursive binder *)
+Check ∀ '((x,y) as z), x+y=0/\z=z.        (* Other example of recursive binder, now treated as the exists case *)
-- 
cgit v1.2.3


From e4d93d1cef27d3a8c1e36139fc1e118730406f67 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 17 Aug 2017 20:12:55 +0200
Subject: Adding general support for irrefutable disjunctive patterns.

This now works not only for parsing of fun/forall (as in 8.6), but
also for arbitraty notations with binders and for printing.
---
 test-suite/output/Notations3.out | 8 ++++++++
 test-suite/output/Notations3.v   | 7 +++++++
 2 files changed, 15 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 0463e5bfbd..fa4ff3be64 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -209,3 +209,11 @@ exists '({{x, y}} as z), x + y = 0 /\ z = z
      : Prop
 ∀ '({{x, y}} as z), x + y = 0 /\ z = z
      : Prop
+fun '({{{{x, y}}, true}} | {{{{x, y}}, false}}) => x + y
+     : nat * nat * bool -> nat
+myexists ({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y
+     : Prop
+exists '({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y
+     : Prop
+∀ '({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y
+     : Prop
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 9ec459ed69..9f6302f6f2 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -376,3 +376,10 @@ Check fun '((x,y) as z) => x+y=0/\z=z.    (* Primitive fun/forall *)
 Check myexists ((x,y) as z), x+y=0/\z=z.  (* Isolated binding pattern *)
 Check exists '((x,y) as z), x+y=0/\z=z.   (* Applicative recursive binder *)
 Check ∀ '((x,y) as z), x+y=0/\z=z.        (* Other example of recursive binder, now treated as the exists case *)
+
+(* Check parsability and printability of irrefutable disjunctive patterns *)
+
+Check fun '(((x,y),true)|((x,y),false)) => x+y.
+Check myexists (((x,y),true)|((x,y),false)), x>y.
+Check exists '(((x,y),true)|((x,y),false)), x>y.
+Check ∀ '(((x,y),true)|((x,y),false)), x>y.
-- 
cgit v1.2.3


From 5806b0476a1ac9b903503641cc3e2997d3e8d960 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 24 Aug 2017 15:18:23 +0200
Subject: When printing a notation with "match", more flexibility in matching
 equations.

We reason up to order, and accept to match a final catch-all clauses
with any other clause.

This allows for instance to parse and print a notation of the form
"if t is S n then p else q".
---
 test-suite/output/Notations3.out | 4 ++++
 test-suite/output/Notations3.v   | 8 ++++++++
 2 files changed, 12 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index fa4ff3be64..6d195b5122 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -217,3 +217,7 @@ exists '({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y
      : Prop
 ∀ '({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y
      : Prop
+fun p : nat => if p is S n then n else 0
+     : nat -> nat
+fun p : comparison => if p is Lt then 1 else 0
+     : comparison -> nat
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 9f6302f6f2..b4ad4a7b3c 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -383,3 +383,11 @@ Check fun '(((x,y),true)|((x,y),false)) => x+y.
 Check myexists (((x,y),true)|((x,y),false)), x>y.
 Check exists '(((x,y),true)|((x,y),false)), x>y.
 Check ∀ '(((x,y),true)|((x,y),false)), x>y.
+
+(* Check Georges' printability of a "if is then else" notation *)
+
+Notation "'if' c 'is' p 'then' u 'else' v" :=
+  (match c with p => u | _ => v end)
+  (at level 200, p pattern at level 100).
+Check fun p => if p is S n then n else 0.
+Check fun p => if p is Lt then 1 else 0.
-- 
cgit v1.2.3


From dcfd5c2c2cefcd8ae6a5b2e90fcbd98da4f1b120 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 25 Nov 2017 20:50:03 +0100
Subject: Notations: Adding modifiers to tell which kind of binder a constr can
 parse.

Concretely, we provide "constr as ident", "constr as strict pattern"
and "constr as pattern".

This tells to parse a binder as a constr, restricting to only ident or
to only a strict pattern, or to a pattern which can also be an ident.

The "strict pattern" modifier allows to restrict the use of patterns
in printing rules. This allows e.g. to select the appropriate rule for
printing between {x|P} and {'pat|P}.
---
 test-suite/output/Notations3.out |  2 --
 test-suite/output/Notations3.v   |  2 --
 test-suite/success/Notations2.v  | 19 +++++++++++++++++--
 3 files changed, 17 insertions(+), 6 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 6d195b5122..3fd4c1c311 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -194,8 +194,6 @@ pair
             (prod nat (prod nat nat))) (prod (prod nat nat) nat)
 fun x : nat => if x is n .+ 1 then n else 1
      : nat -> nat
-{{{x, y}} : nat * nat | x + y = 0}
-     : Set
 exists2' {{x, y}}, x = 0 & y = 0
      : Prop
 exists2 x : nat * nat,
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index b4ad4a7b3c..9ea218481e 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -341,8 +341,6 @@ Check fun x => if x is n.+1 then n else 1.
 
 (* Examples with binding patterns *)
 
-Check {(x,y)|x+y=0}.
-
 Module D.
 Notation "'exists2'' x , p & q" := (ex2 (fun x => p) (fun x => q))
   (at level 200, x pattern, p at level 200, right associativity,
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index 08d904cea0..7c2cf3ee52 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -98,12 +98,12 @@ Notation "'Funnat' i => t" := (FUNNAT i => t + i%nat) (at level 200).
 
 (* 11. Notations with needed factorization of a recursive pattern *)
 (* See https://github.com/coq/coq/issues/6078#issuecomment-342287412 *)
-Module A.
+Module M11.
 Notation "[:: x1 ; .. ; xn & s ]" := (cons x1 .. (cons xn s) ..).
 Notation "[:: x1 ; .. ; xn ]" := (cons x1 .. (cons xn nil) ..).
 Check [:: 1 ; 2 ; 3 ].
 Check [:: 1 ; 2 ; 3 & nil ]. (* was failing *)
-End A.
+End M11.
 
 (* 12. Preventively check that a variable which does not occur can be instantiated *)
 (* by any term. In particular, it should not be restricted to a binder *)
@@ -111,3 +111,18 @@ Module M12.
 Notation "N ++ x" := (S x) (only parsing).
 Check 2 ++ 0.
 End M12.
+
+(* 13. Check that internal data about associativity are not used in comparing levels *)
+Module M13.
+Notation "x ;; z" := (x + z)
+  (at level 100, z at level 200, only parsing, right associativity).
+Notation "x ;; z" := (x * z)
+  (at level 100, z at level 200, only parsing) : foo_scope.
+End M13.
+
+(* 14. Check that a notation with a "ident" binder does not include a pattern *)
+Module M14.
+Notation "'myexists' x , p" := (ex (fun x => p))
+  (at level 200, x ident, p at level 200, right associativity) : type_scope.
+Check myexists I, I = 0. (* Should not be seen as a constructor *)
+End M14.
-- 
cgit v1.2.3


From 0c4eea2553d5b3b70d0b5baaf92781a544de83bd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 23 Nov 2017 13:30:36 +0100
Subject: Change default for notations with variables bound to both terms and
 binders.

For compatibility, the default is to parse as ident and not as pattern.
---
 test-suite/output/Notations3.out |  6 ++++++
 test-suite/output/Notations3.v   | 12 ++++++++++++
 2 files changed, 18 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 3fd4c1c311..436e97e9fb 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -219,3 +219,9 @@ fun p : nat => if p is S n then n else 0
      : nat -> nat
 fun p : comparison => if p is Lt then 1 else 0
      : comparison -> nat
+fun S : nat => [S | S + S]
+     : nat -> nat * (nat -> nat)
+fun N : nat => [N | N + 0]
+     : nat -> nat * (nat -> nat)
+fun S : nat => [[S | S + S]]
+     : nat -> nat * (nat -> nat)
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 9ea218481e..df3d86793f 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -389,3 +389,15 @@ Notation "'if' c 'is' p 'then' u 'else' v" :=
   (at level 200, p pattern at level 100).
 Check fun p => if p is S n then n else 0.
 Check fun p => if p is Lt then 1 else 0.
+
+(* Check that mixed binders and terms defaults to ident and not pattern *)
+Module E.
+  (* First without an indirection *)
+Notation "[ n | t ]" := (n, (fun n : nat => t)).
+Check fun S : nat => [ S | S+S ].
+Check fun N : nat => (N, (fun n => n+0)). (* another test in passing *)
+  (* Then with an indirection *)
+Notation "[[ n | p | t ]]" := (n, (fun p : nat => t)).
+Notation "[[ n | t ]]" := [[ n | n | t ]].
+Check fun S : nat => [[ S | S+S ]].
+End E.
-- 
cgit v1.2.3


From 9fe03a830ae7b10e1c5fb2b9d41213257bd617f0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 3 Nov 2017 11:48:36 +0100
Subject: Adding notations of the form "{'pat|P}", "exists2 'pat, P & Q", etc.

---
 test-suite/output/Notations3.out | 12 +++++++++++-
 test-suite/output/Notations3.v   | 27 ++++++++++++++++++++++++---
 2 files changed, 35 insertions(+), 4 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 436e97e9fb..e6a6e0288a 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -194,9 +194,11 @@ pair
             (prod nat (prod nat nat))) (prod (prod nat nat) nat)
 fun x : nat => if x is n .+ 1 then n else 1
      : nat -> nat
+{'{{x, y}} : nat * nat | x + y = 0}
+     : Set
 exists2' {{x, y}}, x = 0 & y = 0
      : Prop
-exists2 x : nat * nat,
+myexists2 x : nat * nat,
   let '{{y, z}} := x in y > z & let '{{y, z}} := x in z > y
      : Prop
 fun '({{x, y}} as z) => x + y = 0 /\ z = z
@@ -225,3 +227,11 @@ fun N : nat => [N | N + 0]
      : nat -> nat * (nat -> nat)
 fun S : nat => [[S | S + S]]
      : nat -> nat * (nat -> nat)
+{I : nat | I = I}
+     : Set
+{'I : True | I = I}
+     : Prop
+{'{{x, y}} : nat * nat | x + y = 0}
+     : Set
+exists2 '{{y, z}} : nat * nat, y > z & z > y
+     : Prop
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index df3d86793f..f41ddac4d4 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -341,6 +341,10 @@ Check fun x => if x is n.+1 then n else 1.
 
 (* Examples with binding patterns *)
 
+Import SpecifPatternNotations.
+
+Check {'(x,y)|x+y=0}.
+
 Module D.
 Notation "'exists2'' x , p & q" := (ex2 (fun x => p) (fun x => q))
   (at level 200, x pattern, p at level 200, right associativity,
@@ -353,7 +357,15 @@ End D.
 (* Ensuring for reparsability that printer of notations does not use a
    pattern where only an ident could be reparsed *)
 
-Check ex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y).
+Module E.
+Inductive myex2 {A:Type} (P Q:A -> Prop) : Prop :=
+  myex_intro2 : forall x:A, P x -> Q x -> myex2 P Q.
+Notation "'myexists2' x : A , p & q" := (myex2 (A:=A) (fun x => p) (fun x => q))
+  (at level 200, x ident, A at level 200, p at level 200, right associativity,
+    format "'[' 'myexists2'  '/  ' x  :  A ,  '/  ' '[' p  &  '/' q ']' ']'")
+  : type_scope.
+Check myex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y).
+End E.
 
 (* A canonical example of a notation with a non-recursive binder *)
 
@@ -391,7 +403,7 @@ Check fun p => if p is S n then n else 0.
 Check fun p => if p is Lt then 1 else 0.
 
 (* Check that mixed binders and terms defaults to ident and not pattern *)
-Module E.
+Module F.
   (* First without an indirection *)
 Notation "[ n | t ]" := (n, (fun n : nat => t)).
 Check fun S : nat => [ S | S+S ].
@@ -400,4 +412,13 @@ Check fun N : nat => (N, (fun n => n+0)). (* another test in passing *)
 Notation "[[ n | p | t ]]" := (n, (fun p : nat => t)).
 Notation "[[ n | t ]]" := [[ n | n | t ]].
 Check fun S : nat => [[ S | S+S ]].
-End E.
+End F.
+
+(* Check parsability/printability of {x|P} and variants *)
+
+Check {I:nat|I=I}.
+Check {'I:True|I=I}.
+Check {'(x,y)|x+y=0}.
+
+(* Check exists2 with a pattern *)
+Check ex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y).
-- 
cgit v1.2.3


From 0af54860172efe1aa5da419b81e4cb34348320ee Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 23 Nov 2017 13:42:41 +0100
Subject: Trying a hack to support {'pat|P} without breaking compatibility.

Concretely, we bypass the following limitation: The notation
"{ ' pat | P }" broke the parsing of expressions of the form
"{ forall x, P } + { Q }". Indeed the latter works thanks to a
tolerance of Camlp5 in parsing "forall x, P" at level 200 while the
rule asks to actually parse the interior of "{ ... }" at level 99 (the
reason for 99 is to be below the rule for "M : T" which is at level
100, so that "{ x : A | P }" does not see "x : A" as a cast). Adding
an extra "'"; pat = pattern in parallel to c = constr LEVEL "99" broke
the tolerance for constr at level 200.

We fix this by adding an ad hoc rule for "{ binder_constr }" in the
native grammar (g_constr.ml4).

Actually, this is inconsistent with having a rule for "{ constr at level 99 }"
in Notations.v. We should have both rules in Notations.v or both rules
hard-wired in the native grammar. But I still don't know what is the best
decision to take, so leaving as it at the current time.

Advantages of hard-wiring both rules in g_constr.ml4: a bit simpler in
metasyntax.ml (no need to ensure that the rule exist). Disadvantages:
if one wants a different initial state without the business needing
the "{ }" for sumbool, sumor, sig, sigT, one still have the rules
there.

Advantages of having them in Notations.v: more modular, we can change
the initial state. Disadvantages: one would need a new kind of
modifier, something like "x at level 99 || binder_constr", with all
the difficulty to find a nice, intuitive, name for "binder_constr",
and the difficulty of understanding if there is a generality to this
"||" disjunction operator, and whether it should be documented or not.
---
 test-suite/output/Notations3.v | 2 --
 1 file changed, 2 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index f41ddac4d4..c98bfff413 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -341,8 +341,6 @@ Check fun x => if x is n.+1 then n else 1.
 
 (* Examples with binding patterns *)
 
-Import SpecifPatternNotations.
-
 Check {'(x,y)|x+y=0}.
 
 Module D.
-- 
cgit v1.2.3


From 2aff5c40ba9b40b4e0188b799dde6f31585e356b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 6 Dec 2017 10:01:24 +0100
Subject: Adding a test for wish #5532.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5532.v b/test-suite/bugs/closed/5532.v
new file mode 100644
index 0000000000..ee5446e548
--- /dev/null
+++ b/test-suite/bugs/closed/5532.v
@@ -0,0 +1,15 @@
+(* A wish granted by the new support for patterns in notations *)
+
+Local Notation mkmatch0 e p
+  := match e with
+     | p => true
+     | _ => false
+     end.
+Local Notation "'mkmatch' [[ e ]] [[ p ]]"
+  := match e with
+     | p => true
+     | _ => false
+     end
+       (at level 0, p pattern).
+Check mkmatch0 _ ((0, 0)%core).
+Check mkmatch [[ _ ]] [[ ((0, 0)%core) ]].
-- 
cgit v1.2.3