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

6 files changed, 21 insertions, 5 deletions

diff --git a/dev/TODO b/dev/TODO
index ca3b7c992..b27cac28e 100644
--- a/dev/TODO
+++ b/dev/TODO
@@ -1,4 +1,7 @@
 
+ o Termes
+     - introduire un constructeur pour les variables existentielles
+
  o Lib
      - écrire une fonction d'export qui supprimme les FrozenState,
        vérifie qu'il n'y a pas de section ouvert, et présente les
@@ -17,6 +20,7 @@
      - utiliser DOPL plutôt que DOPN (sauf pour Case)
      - batch mode => pas de undo, ni de reset
      - conversion : déplier la constante la plus récente
+     - un cache pour type_of_const, type_of_inductive, type_of_constructor
 
  o Lexer
      à compléter
diff --git a/kernel/typing.ml b/kernel/typing.ml
index dfce2e442..46fbbf17c 100644
--- a/kernel/typing.ml
+++ b/kernel/typing.ml
@@ -415,6 +415,8 @@ let add_mind sp mie env =
   in
   add_mind sp mib (add_constraints cst env)
 
+let add_constraints = add_constraints
+
 let export = export
 let import = import
 
diff --git a/kernel/typing.mli b/kernel/typing.mli
index a960b78dd..f93494a95 100644
--- a/kernel/typing.mli
+++ b/kernel/typing.mli
@@ -36,6 +36,7 @@ val add_parameter :
   section_path -> constr -> 'a environment -> 'a environment
 val add_mind : 
   section_path -> mutual_inductive_entry -> 'a environment -> 'a environment
+val add_constraints : constraints -> 'a environment -> 'a environment
 
 val lookup_var : identifier -> 'a environment -> name * typed_type
 val lookup_rel : int -> 'a environment -> name * typed_type
diff --git a/library/declare.ml b/library/declare.ml
index 1af5ad6a8..79588e750 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 7ffbd2110..f7fac0313 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 9436e446b..e959c6091 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