Types inductifs parametriques

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

2 files changed, 6 insertions, 5 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 6bace2654..1b48acf04 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -43,9 +43,9 @@ let string_of_strength = function
   | Global -> "(global)"
 
 (* XML output hooks *)
-let xml_declare_variable = ref (fun sp -> ())
-let xml_declare_constant = ref (fun sp -> ())
-let xml_declare_inductive = ref (fun sp -> ())
+let xml_declare_variable = ref (fun (sp:object_name) -> ())
+let xml_declare_constant = ref (fun (sp:bool * constant)-> ())
+let xml_declare_inductive = ref (fun (sp:bool * object_name) -> ())
 
 let if_xml f x = if !Options.xml_export then f x else ()
 
@@ -291,7 +291,6 @@ let discharge_inductive ((sp,kn),(dhyps,imps,mie)) =
         Discharge.process_inductive sechyps repl mie)
 
 let dummy_one_inductive_entry mie = {
-  mind_entry_params = [];
   mind_entry_typename = mie.mind_entry_typename;
   mind_entry_arity = mkProp;
   mind_entry_consnames = mie.mind_entry_consnames;
@@ -300,6 +299,7 @@ let dummy_one_inductive_entry mie = {
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
 let dummy_inductive_entry (_,imps,m) = ([],imps,{
+  mind_entry_params = [];
   mind_entry_record = false;
   mind_entry_finite = true;
   mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds })
diff --git a/library/library.ml b/library/library.ml
index ce4fa533c..456658760 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -308,7 +308,8 @@ let (in_import, out_import) =
 (*s Loading from disk to cache (preparation phase) *)
 
 let vo_magic_number7 = 07992 (* V8.0 final old syntax *)
-let vo_magic_number8 = 08002 (* V8.0 final new syntax *)
+(* let vo_magic_number8 = 08002 (* V8.0 final new syntax *) *)
+let vo_magic_number8 = 08003 (* V8.0 final new syntax + new params in ind *)
 
 let (raw_extern_library7, raw_intern_library7) =
   System.raw_extern_intern vo_magic_number7 ".vo"