Changement 'as notation' en 'where notation'

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

2 files changed, 9 insertions, 9 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 49f8b0d85..0c79c9973 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -148,8 +148,8 @@ GEXTEND Gram
     [ [ ","; nal = LIST1 base_ident SEP "," -> nal | -> [] ] ]
   ;
   decl_notation:
-    [ [ "as"; ntn = STRING; scopt = OPT [ ":"; sc = IDENT -> sc] -> 
-        (ntn,scopt) ] ]
+    [ [ "where"; ntn = STRING; ":="; c = constr; 
+         scopt = OPT [ ":"; sc = IDENT -> sc] -> (ntn,c,scopt) ] ]
   ;
   type_option:
     [ [ ":"; c = constr -> c 
@@ -228,7 +228,7 @@ GEXTEND Gram
   ;
   oneind:
     [ [ id = base_ident; indpar = simple_binders_list; ":"; c = constr; 
-        ntn = OPT decl_notation ; ":="; lc = constructor_list ->
+        ":="; lc = constructor_list; ntn = OPT decl_notation ->
 	  (id,ntn,indpar,c,lc) ] ]
   ;
   simple_binders_list:
@@ -252,7 +252,7 @@ GEXTEND Gram
   ;
   onerec:
     [ [ id = base_ident; bl = ne_fix_binders; ":"; type_ = constr;
-        ntn = OPT decl_notation; ":="; def = constr ->
+        ":="; def = constr; ntn = OPT decl_notation ->
           let ni = List.length (List.flatten (List.map fst bl)) - 1 in
           let loc0 = fst (List.hd (fst (List.hd bl))) in
           let loc1 = join_loc loc0 (constr_loc type_) in
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 7475566b7..3955d15f8 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -28,7 +28,7 @@ open Vernac_
 open Module
 
 
-let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "..." ]
+let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "..."; "where" ]
 let _ = 
   if not !Options.v7 then
     List.iter (fun s -> Lexer.add_token ("",s)) vernac_kw
@@ -181,13 +181,13 @@ GEXTEND Gram
       | -> None ] ]
   ;
   decl_notation:
-    [ [ OPT [ "as"; ntn = STRING; scopt = OPT [ ":"; sc = IDENT -> sc]
-               -> (ntn,scopt) ] ] ]
+    [ [ OPT [ "where"; ntn = STRING; ":="; c = constr; 
+         scopt = OPT [ ":"; sc = IDENT -> sc] -> (ntn,c,scopt) ] ] ]
     ;
   (* Inductives and records *)
   inductive_definition:
     [ [ id = base_ident; indpar = LIST0 binder_let; ":"; c = lconstr; 
-        ntn = decl_notation; ":="; lc = constructor_list ->
+        ":="; lc = constructor_list; ntn = decl_notation ->
 	  (id,ntn,indpar,c,lc) ] ]
   ;
   constructor_list:
@@ -208,7 +208,7 @@ GEXTEND Gram
   rec_definition:
     [ [ id = base_ident; bl = LIST1 binder_nodef;
         annot = OPT rec_annotation; type_ = type_cstr; 
-	ntn = decl_notation; ":="; def = lconstr ->
+	":="; def = lconstr; ntn = decl_notation ->
           let names = List.map snd (List.flatten (List.map fst bl)) in
           let ni =
             match annot with