From 366fa1bdea12b522c98984f50428ef8aa48cf8d0 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 9 Oct 2006 16:11:01 +0000
Subject: Notations: - prise en compte des variables liées non liées par la
 notation (bug #1186), - test pour affichage des notations aussi sur les
 sous-ensembles   des lieurs multiples (cf notation "#" dans
 output/Notations.v), - extension, correction et uniformisation de quelques
 fonctions sur   les constr_expr et cases_pattern (avec incidences sur
 rawterm.ml,   parsing et contrib/interface).
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9226 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/output/Notations.out |  6 ++++++
 test-suite/output/Notations.v   | 17 +++++++++++++++++
 2 files changed, 23 insertions(+)

(limited to 'test-suite/output')

diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index e8e206791..975e2ffdf 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -14,6 +14,12 @@ forall n : nat, n = 0
      : Prop
 !(0 = 0)
      : Prop
+forall n : nat, #(n = n)
+     : Prop
+forall n n0 : nat, ##(n = n0)
+     : Prop
+forall n n0 : nat, ###(n = n0)
+     : Prop
 3 + 3
      : Z
 3 + 3
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index 93ccf7a8c..1d24e70a1 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -27,6 +27,23 @@ Check forall n:nat, 0=0.
 
 End A.
 
+(**********************************************************************)
+(* Behaviour wrt to binding variables (cf bug report #1186)           *)
+
+Section B.
+
+Notation "# A" := (forall n:nat, n=n->A) (at level 60).
+Check forall n:nat, # (n=n).
+
+Notation "## A" := (forall n n0:nat, n=n0->A) (at level 60).
+Check forall n n0:nat, ## (n=n0).
+
+Notation "### A" :=
+ (forall n n0:nat, match n with O => True | S n => n=n0 end ->A) (at level 60).
+Check forall n n0:nat, ### (n=n0).
+
+End B.
+
 (**********************************************************************)
 (* Conflict between notation and notation below coercions             *)
 
-- 
cgit v1.2.3