diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-08-10 18:55:49 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-08-10 18:55:49 +0000 |
commit | 6e73985638377a9279d8d4680f790c1cb475df93 (patch) | |
tree | e877432001676654e146b8d74fdcf2b51a03da5b /test-suite/output/Notations.out | |
parent | 95b8610e0671cac9a31dca3fbb238d473c777aa7 (diff) |
Partly revert commit r14389 about relaxing the condition for being a keyword
(it does not work)
Indeed, if a rule in operconstr at some level starts with an ident, it
has to be declared as a keyword because other rules whose leftmost
call is a call to operconstr will eventually the top level "200" even
thought this leftmost operconstr might be declared at a lower
level. This is for instance the reason why "True /\ forall x, x=0" is
parsed even though /\ expects arguments at level less than 80 and
forall is at level 200.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14399 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/output/Notations.out')
-rw-r--r-- | test-suite/output/Notations.out | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 8af9ca82c..72264d082 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -2,8 +2,10 @@ 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) @@ -26,14 +28,17 @@ 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 @@ -75,6 +80,7 @@ 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|] |