Correction de quelques défauts d'affichage (notations sous "as" pour

filtrage; sauts de line intempestifs dans pretty.ml)



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

4 files changed, 23 insertions, 6 deletions

diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 3c440b9d02..9d0d06580d 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -6,7 +6,6 @@ fix F (t : t) : P t :=
   end
      : forall P : t -> Type,
        (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
-
 proj = 
 fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) =>
 match eq_nat_dec x y with
@@ -18,5 +17,14 @@ match eq_nat_dec x y with
 end
      : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
 
-
 Argument scopes are [nat_scope nat_scope _ _ _]
+foo = 
+fix foo (A : Type) (l : list A) {struct l} : option A :=
+  match l with
+  | nil => None (A:=A)
+  | x0 :: nil => Some x0
+  | x0 :: (_ :: _) as l0 => foo A l0
+  end
+     : forall A : Type, list A -> option A
+
+Argument scopes are [type_scope list_scope]
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 56d5cfb4e7..61f89d403a 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -20,3 +20,16 @@ Definition proj (x y:nat) (P:nat -> Type) (def:P x) (prf:P y) : P y :=
  end.
 
 Print proj.
+
+(* Use notations even below aliases *)
+
+Require Import List.
+
+Fixpoint foo (A:Type) (l:list A) : option A :=
+  match l with
+  | nil => None
+  | x0 :: nil => Some x0
+  | x0 :: (x1 :: xs) as l0 => foo A l0
+  end.
+
+Print foo.
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index 7949ef7b2c..ecfe85054b 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -5,7 +5,6 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I
 d2 = fun x : nat => d1 (y:=x)
      : forall x x0 : nat, x0 = x -> x0 = x
 
-
 Arguments x, x0 are implicit
 Argument scopes are [nat_scope nat_scope _]
 map id (1 :: nil)
diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out
index 41e8648bc0..f94ed64234 100644
--- a/test-suite/output/TranspModtype.out
+++ b/test-suite/output/TranspModtype.out
@@ -1,10 +1,7 @@
 TrM.A = M.A
      : Set
-
 OpM.A = M.A
      : Set
-
 TrM.B = M.B
      : Set
-
 *** [ OpM.B : Set ]