petits changements de syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4860 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 14 insertions, 2 deletions

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index cdb9574e6..5fe640cc5 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -542,15 +542,27 @@ let make_anon_notation symbols =
 let make_symbolic n symbols etyps =
   ((n,List.map (assoc_of_type n) etyps), make_anon_notation symbols)
 
+let is_not_small_constr = function
+    ETConstr _ -> true
+  | ETOther("constr","binder_constr") -> true
+  | _ -> false
+
 let rec define_keywords = function
-    NonTerm(_,Some(_,(ETConstr _|ETOther("constr","binder_constr")))) as n1 ::
-    Term("IDENT",k) :: l when not !Options.v7 ->
+    NonTerm(_,Some(_,e)) as n1 :: Term("IDENT",k) :: l
+     when not !Options.v7 && is_not_small_constr e ->
       prerr_endline ("Defining '"^k^"' as keyword");
       Lexer.add_token("",k);
       n1 :: Term("",k) :: define_keywords l
   | n :: l -> n :: define_keywords l
   | [] -> []
 
+let define_keywords = function
+    Term("IDENT",k)::l when not !Options.v7 ->
+      prerr_endline ("Defining '"^k^"' as keyword");
+      Lexer.add_token("",k);
+      Term("",k) :: define_keywords l
+  | l -> define_keywords l
+
 let make_production etyps symbols =
   let prod =
     List.fold_right