From 39608a87309670aff4895295b0ffbeec932e11e5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 10 Aug 2001 16:37:49 +0000
Subject: Hack rapide pour réduire significativement la taille des vo

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1893 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/declare.ml | 23 +++++++++++++++++++++--
 1 file changed, 21 insertions(+), 2 deletions(-)

diff --git a/library/declare.ml b/library/declare.ml
index b360d8e01b..ca1cea16af 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -176,7 +176,12 @@ let load_constant (sp,(ce,stre,op)) =
 let open_constant (sp,_) =
   Nametab.push_short_name (basename sp) (ConstRef sp)
 
-let export_constant x = Some x
+(* Hack to reduce the size of .vo: we keep only what load/open needs *)
+let dummy_constant_entry = ConstantEntry { 
+  const_entry_body = mkProp;
+  const_entry_type = None }
+
+let export_constant (ce,stre,op) = Some (dummy_constant_entry,stre,op)
 
 let (in_constant, out_constant) =
   let od = {
@@ -241,7 +246,21 @@ let open_inductive (sp,mie) =
   let names = inductive_names sp mie in
   List.iter (fun (sp, ref) -> Nametab.push_short_name (basename sp) ref) names
 
-let export_inductive x = Some x
+let dummy_one_inductive_entry mie = {
+  mind_entry_nparams = 0;
+  mind_entry_params = [];
+  mind_entry_typename = mie.mind_entry_typename;
+  mind_entry_arity = mkProp;
+  mind_entry_consnames = mie.mind_entry_consnames;
+  mind_entry_lc = []
+}
+
+(* Hack to reduce the size of .vo: we keep only what load/open needs *)
+let dummy_inductive_entry m = {
+  mind_entry_finite = true;
+  mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds }
+
+let export_inductive x = Some (dummy_inductive_entry x)
 
 let (in_inductive, out_inductive) =
   let od = {
-- 
cgit v1.2.3