From 398358618bb3eabfe822b79c669703c1c33b67e6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
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/output')

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 9c711ff26..5bb77b8fd 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 d81cc702a..201198b3e 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