ajout des constraintes pendant le chargement d'un module (load)

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

3 files changed, 14 insertions, 5 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 1af5ad6a88..79588e750a 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -3,6 +3,7 @@
 
 open Util
 open Names
+open Constant
 open Inductive
 open Libobject
 open Lib
@@ -42,7 +43,9 @@ let cache_parameter (sp,c) =
   Global.add_parameter sp c;
   Nametab.push (basename sp) sp
 
-let load_parameter _ = ()
+let load_parameter (sp,_) =
+  let cb = Global.lookup_constant sp in
+  Global.add_constraints cb.const_constraints
   
 let open_parameter (sp,_) =
   Nametab.push (basename sp) sp
@@ -69,7 +72,9 @@ let cache_constant (sp,ce) =
   Nametab.push (basename sp) sp;
   declare_constant_implicits sp
 
-let load_constant _ = ()
+let load_constant (sp,_) =
+  let cb = Global.lookup_constant sp in
+  Global.add_constraints cb.const_constraints
   
 let open_constant (sp,_) =
   Nametab.push (basename sp) sp;
@@ -83,7 +88,7 @@ let (in_constant, out_constant) =
     load_function = load_constant;
     open_function = open_constant;
     specification_function = specification_constant } in
-  declare_object ("Parameter", od)
+  declare_object ("Constant", od)
 
 let declare_constant id ce =
   let sp = add_leaf id CCI (in_constant ce) in
@@ -105,7 +110,9 @@ let cache_inductive (sp,mie) =
   push_inductive_names sp mie;
   declare_inductive_implicits sp
 
-let load_inductive _ = ()
+let load_inductive (sp,_) =
+  let mib = Global.lookup_mind sp in
+  Global.add_constraints mib.mind_constraints
   
 let open_inductive (sp,mie) =
   push_inductive_names sp mie;
@@ -119,7 +126,7 @@ let (in_inductive, out_inductive) =
     load_function = load_inductive;
     open_function = open_inductive;
     specification_function = specification_inductive } in
-  declare_object ("Parameter", od)
+  declare_object ("Inductive", od)
 
 let declare_mind mie =
   let id = match mie.mind_entry_inds with
diff --git a/library/global.ml b/library/global.ml
index 7ffbd2110a..f7fac03139 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -29,6 +29,7 @@ let push_rel nac = global_env := push_rel nac !global_env
 let add_constant sp ce = global_env := add_constant sp ce !global_env
 let add_parameter sp c = global_env := add_parameter sp c !global_env
 let add_mind sp mie = global_env := add_mind sp mie !global_env
+let add_constraints c = global_env := add_constraints c !global_env
 
 let lookup_var id = lookup_var id !global_env
 let lookup_rel n = lookup_rel n !global_env
diff --git a/library/global.mli b/library/global.mli
index 9436e446b2..e959c60914 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -29,6 +29,7 @@ val push_rel : name * constr -> unit
 val add_constant : section_path -> constant_entry -> unit
 val add_parameter : section_path -> constr -> unit
 val add_mind : section_path -> mutual_inductive_entry -> unit
+val add_constraints : constraints -> unit
 
 val lookup_var : identifier -> name * typed_type
 val lookup_rel : int -> name * typed_type