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

4 files changed, 30 insertions, 20 deletions

diff --git a/toplevel/record.ml b/toplevel/record.ml
index 3ef7eccad9..10d4e5dc60 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -250,10 +250,19 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls
       mind_entry_consnames = [idbuild];
       mind_entry_lc = [type_constructor] }
   in
+  (* spiwack: raises an error if the structure is supposed to be non-recursive,
+        but isn't *)
+  (* there is probably a way to push this to "declare_mutual" *)
+  begin match  finite with
+  | BiFinite -> 
+      if dependent (mkRel (nparams+1)) (it_mkProd_or_LetIn mkProp fields) then
+	error "Records declared with the keyword Record or Structure cannot be recursive. Maybe you meant to define an Inductive or CoInductive record."
+  | _ -> ()
+  end;
   let mie =
     { mind_entry_params = List.map degenerate_decl params;
       mind_entry_record = true;
-      mind_entry_finite = finite;
+      mind_entry_finite = recursivity_flag_of_kind finite;
       mind_entry_inds = [mie_ind] } in
   let kn = Command.declare_mutual_with_eliminations true mie [(paramimpls,[])] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
@@ -333,7 +342,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
 	cref, [proj_name, Some proj_cst]
     | _ ->
 	let idarg = Nameops.next_ident_away (snd id) (ids_of_context (Global.env())) in
-	let ind = declare_structure true infer (snd id) idbuild paramimpls
+	let ind = declare_structure BiFinite infer (snd id) idbuild paramimpls
 	  params (Option.cata (fun x -> x) (new_Type ()) arity) fieldimpls fields
 	  ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) sign
 	in
@@ -386,16 +395,16 @@ let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuil
     States.with_heavy_rollback (fun () ->
       typecheck_params_and_fields idstruc sc ps notations fs) () in
   let sign = structure_signature (fields@params) in
-    match kind with
-    | Record | Structure ->
-	let arity = Option.default (new_Type ()) sc in
-	let implfs = List.map
-	  (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in
-	let ind = declare_structure finite infer idstruc idbuild implpars params arity implfs fields is_coe coers sign in
-	if infer then search_record declare_record_instance (ConstructRef (ind,1)) sign;
-	IndRef ind	  
+    match kind with	  
     | Class def ->
 	let gr = declare_class finite def infer (loc,idstruc) idbuild 
 	  implpars params sc implfs fields is_coe coers sign in
 	if infer then search_record declare_class_instance gr sign;
 	gr
+    | _ ->
+	let arity = Option.default (new_Type ()) sc in
+	let implfs = List.map
+	  (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in
+	let ind = declare_structure finite infer idstruc idbuild implpars params arity implfs fields is_coe coers sign in
+	if infer then search_record declare_record_instance (ConstructRef (ind,1)) sign;
+	IndRef ind
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 564d4409f0..0e23af5c0f 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -27,7 +27,8 @@ val declare_projections :
   bool list -> manual_explicitation list list -> rel_context -> 
   (name * bool) list * constant option list
 
-val declare_structure : bool (*coinductive?*)-> bool (*infer?*) -> identifier -> identifier -> 
+val declare_structure : Decl_kinds.recursivity_kind -> 
+  bool (*infer?*) -> identifier -> identifier -> 
   manual_explicitation list -> rel_context -> (* params *) constr -> (* arity *)
   Impargs.manual_explicitation list list -> rel_context -> (* fields *)
   ?kind:Decl_kinds.definition_object_kind -> ?name:identifier ->
@@ -37,6 +38,6 @@ val declare_structure : bool (*coinductive?*)-> bool (*infer?*) -> identifier ->
   inductive
 
 val definition_structure :
-  record_kind * bool (*coinductive?*) * bool(*infer?*)* lident with_coercion * local_binder list *
+  inductive_kind * Decl_kinds.recursivity_kind * bool(*infer?*)* lident with_coercion * local_binder list *
   (local_decl_expr with_coercion with_notation) list * 
   identifier * constr_expr option -> global_reference
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 39a545215b..5796d79ee0 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -399,17 +399,17 @@ let vernac_inductive finite infer indl =
 	| _ -> () (* dumping is done by vernac_record (called below) *) )
       indl;
   match indl with
-  | [ ( id , bl , c , Some b, RecordDecl (oc,fs) ), None ] -> 
+  | [ ( id , bl , c , b, RecordDecl (oc,fs) ), None ] -> 
       vernac_record (match b with Class true -> Class false | _ -> b)
 	finite infer id bl c oc fs
-  | [ ( id , bl , c , Some (Class true), Constructors [l]), _ ] -> 
+  | [ ( id , bl , c , Class true, Constructors [l]), _ ] -> 
       let f = 
 	let (coe, ((loc, id), ce)) = l in
 	  ((coe, AssumExpr ((loc, Name id), ce)), None)
       in vernac_record (Class true) finite infer id bl c None [f]
-  | [ ( id , bl , c , Some (Class true), _), _ ] -> 
+  | [ ( id , bl , c , Class true, _), _ ] -> 
       Util.error "Definitional classes must have a single method"
-  | [ ( id , bl , c , Some (Class false), Constructors _), _ ] ->
+  | [ ( id , bl , c , Class false, Constructors _), _ ] ->
       Util.error "Inductive classes not supported"
   | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] -> 
       Util.error "where clause not supported for (co)inductive records"
@@ -418,7 +418,7 @@ let vernac_inductive finite infer indl =
       | _ -> Util.error "Cannot handle mutually (co)inductive records."
     in
     let indl = List.map unpack indl in
-      Command.build_mutual indl finite
+      Command.build_mutual indl (recursivity_flag_of_kind finite)
 
 let vernac_fixpoint l b = 
   if Dumpglob.dump () then
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index aa6a48d66e..b94526a6ea 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -140,7 +140,7 @@ type locality_flag  = bool (* true = Local;         false = Global         *)
 type coercion_flag  = bool (* true = AddCoercion;   false = NoCoercion     *)
 type export_flag    = bool (* true = Export;        false = Import         *)
 type specif_flag    = bool (* true = Specification; false = Implementation *)
-type inductive_flag = bool (* true = Inductive;     false = CoInductive    *)
+type inductive_flag = Decl_kinds.recursivity_kind
 type onlyparsing_flag = bool (* true = Parse only;  false = Print also     *)
 type infer_flag     = bool (* true = try to Infer record; false = nothing  *)
 
@@ -155,7 +155,7 @@ type local_decl_expr =
   | AssumExpr of lname * constr_expr
   | DefExpr of lname * constr_expr * constr_expr option
 
-type record_kind = Record | Structure | Class of bool (* true = definitional, false = inductive *)
+type inductive_kind = Inductive_kw | CoInductive | Record | Structure | Class of bool (* true = definitional, false = inductive *)
 type decl_notation = (string * constr_expr * scope_name option) option
 type simple_binder = lident list  * constr_expr
 type class_binder = lident * constr_expr list
@@ -166,7 +166,7 @@ type constructor_list_or_record_decl_expr =
   | Constructors of constructor_expr list
   | RecordDecl of lident option * local_decl_expr with_coercion with_notation list
 type inductive_expr =
-  lident with_coercion * local_binder list * constr_expr option * record_kind option * 
+  lident with_coercion * local_binder list * constr_expr option * inductive_kind * 
     constructor_list_or_record_decl_expr
 
 type module_binder = bool option * lident list * module_type_ast