diff options
| author | herbelin | 2011-04-27 09:30:03 +0000 |
|---|---|---|
| committer | herbelin | 2011-04-27 09:30:03 +0000 |
| commit | 02f94d8b86cb3ee6453a914fc5f512005e0a591f (patch) | |
| tree | e3419b9ef4a7746c01ea2d7d92fee3935144e768 | |
| parent | 14a3a6fadeb96cd25e4f58de44130b569e8b748d (diff) | |
Fixing output of Notations2.v test messed up in r14060
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14071 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | test-suite/output/Notations2.out | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 2e0e145e1a..d92f8d6946 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -14,6 +14,7 @@ fun (P : nat -> nat -> Prop) (x : nat) => exists x0, P x x0 : (nat -> nat -> Prop) -> nat -> Prop ∃ n p : nat, n + p = 0 : Prop +let a := 0 in ∃ x y : nat, let b := 1 in let c := b in @@ -30,7 +31,7 @@ let d := 2 in ∃ z : nat, let e := 3 in let f := 4 in x + y = z + d λ A : Type, ∀ n p : A, n = p : Type -> Prop Defining 'let'' as keyword -let' f (x y : nat) (a:=0) (z : nat) (_ : bool) := x + y + z + 1 in (f(0)) 1 2 +let' f (x y : nat) (a:=0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2 : bool -> nat λ (f : nat -> nat) (x : nat), f(x) + S(x) : (nat -> nat) -> nat -> nat |