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

3 files changed, 28 insertions, 16 deletions

diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 8af9ca82ca..72264d082b 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|]
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index f4eaeb4788..d92f8d6946 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -30,6 +30,7 @@ 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)
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 551ff302ae..00ad678593 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -308,6 +308,7 @@ let rec interp_list_parser hd = function
       xyl, List.rev_append hd tl'
   | SProdList _ :: _ -> anomaly "Unexpected SProdList in interp_list_parser"
 
+
 (* Find non-terminal tokens of notation *)
 
 (* To protect alphabetic tokens and quotes from being seen as variables *)
@@ -575,24 +576,28 @@ let hunks_of_format (from,(vars,typs)) symfmt =
 
 let assoc_of_type n (_,typ) = precedence_of_entry_type n typ
 
-let constr_level n = function
-  | ETConstr (NextLevel,_) -> n-1
-  | ETConstr (NumLevel n,_) -> n
-  | ETOther("constr","binder_constr") -> 200
-  | _ -> 0
+let is_not_small_constr = function
+    ETConstr _ -> true
+  | ETOther("constr","binder_constr") -> true
+  | _ -> false
 
-  (* Ensure that IDENT articulation terminal symbols are keywords *)
-let rec define_keywords n = function
-  | GramConstrNonTerminal(e,Some _) as x1 :: GramConstrTerminal(IDENT k) :: l
-      when constr_level n e > 9 ->
-      (* an entry can catch an ident coming next if it is at a level *)
-      (* higher than the level of applications which is 10 *)
+let rec define_keywords_aux = function
+  | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l
+      when is_not_small_constr e ->
       message ("Defining '"^k^"' as keyword");
       Lexer.add_keyword k;
-      x1 :: GramConstrTerminal(KEYWORD k) :: define_keywords n l
-  | x :: l -> x :: define_keywords  n l
+      n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
+  | n :: l -> n :: define_keywords_aux l
   | [] -> []
 
+  (* Ensure that IDENT articulation terminal symbols are keywords *)
+let define_keywords = function
+  | GramConstrTerminal(IDENT k)::l ->
+      message ("Defining '"^k^"' as keyword");
+      Lexer.add_keyword k;
+      GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
+  | l -> define_keywords_aux l
+
 let distribute a ll = List.map (fun l -> a @ l) ll
 
   (* Expand LIST1(t,sep) into the combination of t and t;sep;LIST1(t,sep)
@@ -610,7 +615,7 @@ let rec expand_list_rule typ tkl x n i hds ll =
     distribute (GramConstrListMark (i+1,false) :: hds @ [main]) ll @
       expand_list_rule typ tkl x n (i+1) (main :: tks @ hds) ll
 
-let make_production n etyps symbols =
+let make_production etyps symbols =
   let prod =
     List.fold_right
       (fun t ll -> match t with
@@ -634,7 +639,7 @@ let make_production n etyps symbols =
             | _ ->
                 error "Components of recursive patterns in notation must be terms or binders.")
       symbols [[]] in
-  List.map (define_keywords n) prod
+  List.map define_keywords prod
 
 let rec find_symbols c_current c_next c_last = function
   | [] -> []
@@ -1005,7 +1010,7 @@ let recover_notation_syntax rawntn =
 
 let make_pa_rule (n,typs,symbols,_) ntn =
   let assoc = recompute_assoc typs in
-  let prod = make_production n typs symbols in
+  let prod = make_production typs symbols in
   (n,assoc,ntn,prod)
 
 let make_pp_rule (n,typs,symbols,fmt) =