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


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9226 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 23 insertions, 0 deletions

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
@@ -28,6 +28,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             *)
 
 (* Case of a printer conflict *)