diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-21 12:14:28 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-21 12:16:07 +0200 |
| commit | 9aa960939cb02e655b40d67f42a3df2bcf3f73c3 (patch) | |
| tree | c28a6e8ac9150ef2ffe122b23cd9044fa948c6f9 /test-suite/output/Notations2.out | |
| parent | 968e1eb50813fdcc402f689dbaedfcccceec61df (diff) | |
Adapting output tests to the removal of the new token warning and to
the printing of the context of open evars in Check.
Diffstat (limited to 'test-suite/output/Notations2.out')
| -rw-r--r-- | test-suite/output/Notations2.out | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 958001c39..58ec1de56 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -24,7 +24,6 @@ let d := 2 in ∃ z : nat, let e := 3 in let f := 4 in x + y = z + d : Prop ∀ n p : nat, n + p = 0 : Prop -Identifier 'λ' now a keyword λ n p : nat, n + p = 0 : nat -> nat -> Prop λ (A : Type) (n p : A), n = p @@ -33,7 +32,6 @@ Identifier 'λ' now a keyword : Type -> Prop λ A : Type, ∀ n p : A, n = p : Type -> Prop -Identifier 'let'' now a keyword 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) |