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".

2 files changed, 12 insertions, 0 deletions

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index fa4ff3be6..6d195b512 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 9f6302f6f..b4ad4a7b3 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.