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

3 files changed, 7 insertions, 7 deletions

diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index f0e5c6256c..7e9ba3f8ea 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -1370,12 +1370,12 @@ let do_build_inductive
 	let _time3 = System.get_time () in
 (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
 	let repacked_rel_inds = 
-	  List.map  (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , None, Vernacexpr.Constructors l),ntn )
+	  List.map  (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
 	                  rel_inds
 	in
 	let msg = 		     
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,repacked_rel_inds))
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds))
 	    ++ fnl () ++
 	    msg
 	in
@@ -1385,12 +1385,12 @@ let do_build_inductive
 	let _time3 = System.get_time () in
 (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
 	let repacked_rel_inds = 
-	  List.map  (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , None, Vernacexpr.Constructors l),ntn )
+	  List.map  (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
 	                  rel_inds
 	in
 	let msg = 		     
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,repacked_rel_inds)) 
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds)) 
 	    ++ fnl () ++
 	    Cerrors.explain_exn e
 	in
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 5180bdad27..668a581e1d 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -109,7 +109,7 @@ let convert_one_inductive sp tyi =
   let sp = sp_of_global (IndRef (sp, tyi)) in
   (((false,(dummy_loc,basename sp)),
    convert_env(List.rev params),
-   Some (extern_constr true envpar arity), None,
+   Some (extern_constr true envpar arity), Vernacexpr.Inductive_kw ,
    Constructors (convert_constructors envpar cstrnames cstrtypes)), None);;
 
 (* This function converts a Mutual inductive definition to a Coqast.t.
@@ -121,7 +121,7 @@ let mutual_to_ast_list sp mib =
   let _, l =
     Array.fold_right
       (fun mi (n,l) -> (n+1, (convert_one_inductive sp n)::l)) mipv (0, []) in
-  VernacInductive (mib.mind_finite, false, l)
+  VernacInductive ((if mib.mind_finite then Decl_kinds.Finite else Decl_kinds.CoFinite), false, l)
   :: (implicit_args_to_ast_list sp mipv);;
 
 let constr_to_ast v = 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 71cef59e2f..c8684a9a0e 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1984,7 +1984,7 @@ let rec xlate_vernac =
 (* 	xlate_formula (Option.get c1), record_constructor, *)
 (*          build_record_field_list field_list) *)
    | VernacInductive (isind, _, lmi) ->
-      let co_or_ind = if isind then "Inductive" else "CoInductive" in
+      let co_or_ind = if Decl_kinds.recursivity_flag_of_kind isind then "Inductive" else "CoInductive" in
       let strip_mutind = function
           (((_, (_,s)), parameters, c, _, Constructors constructors), notopt) ->
           CT_ind_spec