Les records déclarés avec Record ne peuvent plus être récursifs (le

comportement est similaire à la 8.1). Les records récursifs peuvent-être 
déclarés avec Inductive et CoInductive, avec les effets idoines sur leur 
nature.

J'ai fait quelques changements dans VernacInductive pour que tout ceci 
fonctionne bien ensemble. Il reste du nettoyage à faire et probablement 
des ajustement dans le Printing.



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

2 files changed, 13 insertions, 12 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index ff6d998e21..03b1466481 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -151,6 +151,8 @@ GEXTEND Gram
       (* Gallina inductive declarations *)
       | f = finite_token;
         indl = LIST1 inductive_definition SEP "with" ->
+	  let (k,f) = f in
+	  let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
           VernacInductive (f,false,indl)
       | IDENT "Boxed";"Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
           VernacFixpoint (recs,true)
@@ -171,7 +173,7 @@ GEXTEND Gram
 	cfs = [ ":="; l = constructor_list_or_record_decl -> l
 	  | -> RecordDecl (None, []) ] ->
 	  let (recf,indf) = b in
-	    VernacInductive (indf,infer,[((oc,name),ps,s,Some recf,cfs),None])
+	    VernacInductive (indf,infer,[((oc,name),ps,s,recf,cfs),None])
   ] ]
   ;
   typeclass_context:
@@ -214,16 +216,16 @@ GEXTEND Gram
     [ ["Inline" -> true |  -> false] ]
   ;
   finite_token:
-    [ [ "Inductive" -> true
-      | "CoInductive" -> false ] ]
+    [ [ "Inductive" -> (Inductive_kw,Finite)
+      | "CoInductive" -> (CoInductive,CoFinite) ] ]
   ;
   infer_token:
     [ [ "Infer" -> true | -> false ] ]
   ;
   record_token:
-    [ [ IDENT "Record" -> (Record,true)
-      | IDENT "Structure" -> (Structure,true) 
-      | IDENT "Class" -> (Class true,true) ] ]
+    [ [ IDENT "Record" -> (Record,BiFinite)
+      | IDENT "Structure" -> (Structure,BiFinite) 
+      | IDENT "Class" -> (Class true,BiFinite) ] ]
   ;
   (* Simple definitions *)
   def_body:
@@ -249,7 +251,7 @@ GEXTEND Gram
     [ [ id = identref; oc = opt_coercion; indpar = binders_let; 
         c = OPT [ ":"; c = lconstr -> c ];
         ":="; lc = constructor_list_or_record_decl; ntn = decl_notation ->
-	   (((oc,id),indpar,c,None,lc),ntn) ] ]
+	   (((oc,id),indpar,c,lc),ntn) ] ]
   ;
   constructor_list_or_record_decl:
     [ [ "|"; l = LIST1 constructor SEP "|" -> Constructors l
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 496af5b6e7..7b3491de22 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -594,10 +594,9 @@ let rec pr_vernac = function
 	    pr_record_decl b c fs in
       let pr_oneind key (((coe,id),indpar,s,k,lc),ntn) =
 	let kw =
-	  match k with
-	  | None -> str key
-	  | Some b -> str (match b with Record -> "Record" | Structure -> "Structure" 
-	    | Class b -> if b then "Definitional Class" else "Class")
+	  str (match k with Record -> "Record" | Structure -> "Structure"  
+		 | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
+		 | Class b -> if b then "Definitional Class" else "Class")
 	in
 	  hov 0 (
 	    kw ++ spc() ++
@@ -608,7 +607,7 @@ let rec pr_vernac = function
 	      str" :=") ++ pr_constructor_list k lc ++ 
 	    pr_decl_notation pr_constr ntn 
       in
-      hov 1 (pr_oneind (if f then "Inductive" else "CoInductive") (List.hd l))
+      hov 1 (pr_oneind (if (Decl_kinds.recursivity_flag_of_kind f) then "Inductive" else "CoInductive") (List.hd l))
       ++ 
       (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))