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

2 files changed, 28 insertions, 0 deletions

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index cb18fa356..0463e5bfb 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 d768b9ba4..9ec459ed6 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 *)