From c6d9d4fb142ef42634be25b60c0995b541e86629 Mon Sep 17 00:00:00 2001
From: Daniel de Rauglaudre
Date: Mon, 15 Feb 2016 16:22:45 +0100
Subject: Adding ability to put any pattern in binders, prefixed by a quote.

Cf CHANGES for details.
---
 test-suite/output/Binder.out | 8 ++++++++
 test-suite/output/Binder.v   | 7 +++++++
 2 files changed, 15 insertions(+)
 create mode 100644 test-suite/output/Binder.out
 create mode 100644 test-suite/output/Binder.v

(limited to 'test-suite')

diff --git a/test-suite/output/Binder.out b/test-suite/output/Binder.out
new file mode 100644
index 0000000000..34558e9a6b
--- /dev/null
+++ b/test-suite/output/Binder.out
@@ -0,0 +1,8 @@
+foo = fun '(x, y) => x + y
+     : nat * nat -> nat
+forall '(a, b), a /\ b
+     : Prop
+foo = λ '(x, y), x + y
+     : nat * nat → nat
+∀ '(a, b), a ∧ b
+     : Prop
diff --git a/test-suite/output/Binder.v b/test-suite/output/Binder.v
new file mode 100644
index 0000000000..9aced9f665
--- /dev/null
+++ b/test-suite/output/Binder.v
@@ -0,0 +1,7 @@
+Definition foo '(x,y) := x + y.
+Print foo.
+Check forall '(a,b), a /\ b.
+
+Require Import Utf8.
+Print foo.
+Check forall '(a,b), a /\ b.
-- 
cgit v1.2.3