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.

2 files changed, 15 insertions, 0 deletions

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