diff options
| author | herbelin | 2011-08-08 23:04:18 +0000 |
|---|---|---|
| committer | herbelin | 2011-08-08 23:04:18 +0000 |
| commit | ea09770efde4a7bdd573407a408e54ec2b41b6ad (patch) | |
| tree | 46b3d831db010166446a9915ae3f11b02dbf50ee /test-suite | |
| parent | 5184fde1c73ac58364df8a60442dbaaba9685555 (diff) | |
Be a bit less aggressive in declaring idents as keywords in notations
(an articulating ident needs to be a keyword if the constr entry that
preceeds it is higher than the level of applications).
Also fixed is_ident_not_keyword which only looked at the first letter
and at the keyword status to decide if a token is an ident. This
allowed to simplified define_keywords in Metasyntax.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14389 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations.out | 6 | ||||
| -rw-r--r-- | test-suite/output/Notations2.out | 1 |
2 files changed, 0 insertions, 7 deletions
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 72264d082b..8af9ca82ca 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -2,10 +2,8 @@ true ? 0; 1 : nat if true as x return (x ? nat; bool) then 0 else true : nat -Defining 'proj1' as keyword fun e : nat * nat => proj1 e : nat * nat -> nat -Defining 'decomp' as keyword decomp (true, true) as t, u in (t, u) : bool * bool !(0 = 0) @@ -28,17 +26,14 @@ forall n n0 : nat, ###(n = n0) : list nat (1; 2, 4) : nat * nat * nat -Defining 'ifzero' as keyword ifzero 3 : bool -Defining 'pred' as keyword pred 3 : nat fun n : nat => pred n : nat -> nat fun n : nat => pred n : nat -> nat -Defining 'ifn' as keyword Defining 'is' as keyword fun x : nat => ifn x is succ n then n else 0 : nat -> nat @@ -80,7 +75,6 @@ Nil : forall A : Type, list A NIL:list nat : list nat -Defining 'I' as keyword (false && I 3)%bool /\ I 6 : Prop [|1, 2, 3; 4, 5, 6|] diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index d92f8d6946..f4eaeb4788 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -30,7 +30,6 @@ let d := 2 in ∃ z : nat, let e := 3 in let f := 4 in x + y = z + d : Type -> Prop λ 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 : bool -> nat λ (f : nat -> nat) (x : nat), f(x) + S(x) |