Possibilité de syntaxe conjointement à la définition des inductifs et des points-fixes; prise en compte par le traducteur

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

2 files changed, 19 insertions, 10 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 5b88cee39e..4865611a69 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -140,6 +140,10 @@ GEXTEND Gram
   ident_comma_list_tail:
     [ [ ","; nal = LIST1 base_ident SEP "," -> nal | -> [] ] ]
   ;
+  decl_notation:
+    [ [ "as"; ntn = STRING; scopt = OPT [ ":"; sc = IDENT -> sc] -> 
+        (ntn,scopt) ] ]
+  ;
   type_option:
     [ [ ":"; c = constr -> c 
       | -> evar_constr loc ] ]
@@ -216,9 +220,9 @@ GEXTEND Gram
           (id,c,lc) ] ]
   ;
   oneind:
-    [ [ ntn = OPT [ ntn = STRING; ":=" -> (ntn,None) ];
-        id = base_ident; indpar = simple_binders_list; ":"; c = constr; ":=";
-	lc = constructor_list -> (id,ntn,indpar,c,lc) ] ]
+    [ [ id = base_ident; indpar = simple_binders_list; ":"; c = constr; 
+        ntn = OPT decl_notation ; ":="; lc = constructor_list ->
+	  (id,ntn,indpar,c,lc) ] ]
   ;
   simple_binders_list:
     [ [ bl = ne_simple_binders_list -> bl
@@ -241,12 +245,12 @@ GEXTEND Gram
   ;
   onerec:
     [ [ id = base_ident; bl = ne_fix_binders; ":"; type_ = constr;
-        ":="; def = constr ->
+        ntn = OPT decl_notation; ":="; def = constr ->
           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
           let loc2 = join_loc loc0 (constr_loc def) in
-	  (id, ni, CProdN (loc1,bl,type_), CLambdaN (loc2,bl,def)) ] ]
+	  ((id, ni, CProdN (loc1,bl,type_), CLambdaN (loc2,bl,def)), ntn) ] ]
   ;
   specifrec:
     [ [ l = LIST1 onerec SEP "with" -> l ] ]
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 4c62250d23..93de5a0e63 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -171,11 +171,15 @@ GEXTEND Gram
     [ [ IDENT "Eval"; r = Tactic.red_expr; "in" -> Some r
       | -> None ] ]
   ;
+  decl_notation:
+    [ [ OPT [ "as"; ntn = STRING; scopt = OPT [ ":"; sc = IDENT -> sc]
+               -> (ntn,scopt) ] ] ]
+    ;
   (* Inductives and records *)
   inductive_definition:
-    [ [ ntn = OPT [ ntn = STRING -> (ntn,None) ];
-        id = base_ident; indpar = LIST0 simple_binder; ":"; c = lconstr; ":=";
-	lc = constructor_list -> (id,ntn,indpar,c,lc) ] ]
+    [ [ id = base_ident; indpar = LIST0 simple_binder; ":"; c = lconstr; 
+        ntn = decl_notation; ":="; lc = constructor_list ->
+	  (id,ntn,indpar,c,lc) ] ]
   ;
   constructor_list:
     [ [ "|"; l = LIST1 constructor_binder SEP "|" -> l
@@ -194,7 +198,8 @@ GEXTEND Gram
   (* (co)-fixpoints *)
   rec_definition:
     [ [ id = base_ident; bl = LIST1 binder_nodef;
-        annot = OPT rec_annotation; type_ = type_cstr; ":="; def = lconstr ->
+        annot = OPT rec_annotation; type_ = type_cstr; 
+	ntn = decl_notation; ":="; def = lconstr ->
           let names = List.map snd (List.flatten (List.map fst bl)) in
           let ni =
             match annot with
@@ -212,7 +217,7 @@ GEXTEND Gram
           let loc0 = fst (List.hd (fst (List.hd bl))) in
           let loc1 = join_loc loc0 (constr_loc type_) in
           let loc2 = join_loc loc0 (constr_loc def) in
-	  (id, ni, CProdN (loc1,bl,type_), CLambdaN (loc2,bl,def)) ] ]
+	  ((id, ni, CProdN (loc1,bl,type_), CLambdaN (loc2,bl,def)),ntn) ] ]
   ;
   corec_definition:
     [ [ id = base_ident; bl = LIST0 binder_nodef; c = type_cstr; ":=";