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

1 files changed, 10 insertions, 2 deletions

diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 3c440b9d0..9d0d06580 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]