Affichage des notations récursives:

- Prise en compte des notations applicatives
- Remplacement du codage des arguments liste des notations récursives 
  sous forme de terme par une représentation directe (permet notamment
  de résoudre un problème de stack overflow de la fonction d'affichage)
+ Correction bug affichage Lemma dans ppvernac.ml
+ Divers util.ml



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

2 files changed, 20 insertions, 0 deletions

diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 2066a7ef3..6c69c097d 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -50,3 +50,7 @@ Nil
      : forall A : Type, list A
 NIL:list nat
      : list nat
+[|1, 2, 3; 4, 5, 6|]
+     : Z * Z * Z * (Z * Z * Z)
+fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|}:Z
+     : (Z -> Z -> Z -> Z) -> Z
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index 6e637aca3..f19ba998f 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -129,3 +129,19 @@ Check Nil.
 
 Notation NIL := nil.
 Check NIL : list nat.
+
+(**********************************************************************)
+(* Check notations with several recursive patterns                    *)
+
+Notation "[| x , y , .. , z ; a , b , .. , c |]" :=
+  (pair (pair .. (pair x y) .. z) (pair .. (pair a b) .. c)).
+Check [|1,2,3;4,5,6|].
+
+(**********************************************************************)
+(* Test recursive notations involving applications                    *)
+(* Caveat: does not work for applied constant because constants are   *)
+(* classified as notations for the particular constant while this     *)
+(* generic application notation is classified as generic              *)
+
+Notation "{| f ; x ; .. ; y |}" := ( .. (f x) .. y).
+Check fun f => {| f; 0; 1; 2 |} : Z.