Export de l'information si un inductive est un record ou non (pour xml)

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

5 files changed, 10 insertions, 10 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 307c83865..398fed704 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -303,10 +303,10 @@ let declare_inductive_common mie =
   oname
 
 (* for initial declaration *)
-let declare_mind mie =
+let declare_mind isrecord mie =
   let (sp,kn as oname) = declare_inductive_common mie in
   Dischargedhypsmap.set_discharged_hyps sp [] ;
-  !xml_declare_inductive oname;
+  !xml_declare_inductive (isrecord,oname);
   oname
 
 (* when coming from discharge: no xml output *)
diff --git a/library/declare.mli b/library/declare.mli
index 9b268e7ae..85162c04c 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -63,8 +63,8 @@ val redeclare_constant :
 
 (* [declare_mind me] declares a block of inductive types with
    their constructors in the current section; it returns the path of
-   the whole block *)
-val declare_mind : mutual_inductive_entry -> object_name
+   the whole block (boolean must be true iff it is a record) *)
+val declare_mind : bool -> mutual_inductive_entry -> object_name
 
 (* Declaration from Discharge *)
 val redeclare_inductive :
@@ -99,4 +99,4 @@ val strength_of_global : global_reference -> strength
 (* hooks for XML output *)
 val set_xml_declare_variable : (object_name -> unit) -> unit
 val set_xml_declare_constant : (bool * object_name -> unit) -> unit
-val set_xml_declare_inductive : (object_name -> unit) -> unit
+val set_xml_declare_inductive : (bool * object_name -> unit) -> unit
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 9d4e9d68d..fc2c2cb29 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -361,10 +361,10 @@ let interp_mutual lparams lnamearconstrs finite =
   notations, { mind_entry_finite = finite; mind_entry_inds = mispecvec }
   with e -> States.unfreeze fs; raise e
 
-let declare_mutual_with_eliminations mie =
+let declare_mutual_with_eliminations isrecord mie =
   let lrecnames =
     List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
-  let (_,kn) = declare_mind mie in
+  let (_,kn) = declare_mind isrecord mie in
   if_verbose ppnl (minductive_message lrecnames);
   declare_eliminations kn;
   kn
@@ -406,7 +406,7 @@ let extract_coe_la_lc = function
 let build_mutual lind finite =
   let ((coes:identifier list),lparams,lnamearconstructs) = extract_coe_la_lc lind in
   let notations,mie = interp_mutual lparams lnamearconstructs finite in
-  let kn = declare_mutual_with_eliminations mie in
+  let kn = declare_mutual_with_eliminations false mie in
   (* Declare the notations now bound to the inductive types *)
   List.iter (fun (df,c,scope) ->
     Metasyntax.add_notation_interpretation df [] c scope) notations;
diff --git a/toplevel/command.mli b/toplevel/command.mli
index c2db70daf..77eff2b4d 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -41,7 +41,7 @@ val declare_assumption : identifier located list ->
 val build_mutual : inductive_expr list -> bool -> unit
 
 val declare_mutual_with_eliminations :
-  Entries.mutual_inductive_entry -> mutual_inductive
+  bool -> Entries.mutual_inductive_entry -> mutual_inductive
 
 val build_recursive : (fixpoint_expr * decl_notation) list -> unit
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 36d83bb28..acddd2e61 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -228,7 +228,7 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
   let mie =
     { mind_entry_finite = true;
       mind_entry_inds = [mie_ind] } in
-  let sp = declare_mutual_with_eliminations mie in
+  let sp = declare_mutual_with_eliminations true mie in
   let rsp = (sp,0) in (* This is ind path of idstruc *)
   let sp_projs = declare_projections rsp coers fields in
   let build = ConstructRef (rsp,1) in (* This is construct path of idbuild *)