Add type annotations around all calls to Libobject.declare_object

 These annotations are purely optional, but could be quite helpful
 when trying to understand the code, and in particular trying to
 trace which which data-structure may end in the libobject part
 of a vo. By the way, we performed some code simplifications :
  - in Library, a part of the REQUIRE objects was unused.
  - in Declaremods, we removed some checks that were marked as
  useless, this allows to slightly simplify the stored objects.

 To investigate someday : in recordops, the RECMETHODS is storing
 some evar_maps. This is ok for the moment, but might not be in
 the future (cf previous commit on auto hints). This RECMETHODS
 was not detected by my earlier tests : not used in the stdlib ?

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

1 files changed, 9 insertions, 3 deletions

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 0f1b9ac97..994fe33d0 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -43,6 +43,12 @@ type struc_typ = {
 let structure_table = ref (Indmap.empty : struc_typ Indmap.t)
 let projection_table = ref Cmap.empty
 
+(* TODO: could be unify struc_typ and struc_tuple ? in particular,
+   is the inductive always (fst constructor) ? It seems so... *)
+
+type struc_tuple =
+    inductive * constructor * (name * bool) list * constant option list
+
 let load_structure i (_,(ind,id,kl,projs)) =
   let n = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
   let struc =
@@ -75,7 +81,7 @@ let discharge_structure (_,(ind,id,kl,projs)) =
   Some (Lib.discharge_inductive ind, discharge_constructor id, kl,
         List.map (Option.map Lib.discharge_con) projs)
 
-let inStruc =
+let inStruc : struc_tuple -> obj =
   declare_object {(default_object "STRUCTURE") with
     cache_function = cache_structure;
     load_function = load_structure;
@@ -134,7 +140,7 @@ open Libobject
 let load_method (_,(ty,id)) =
   meth_dnet := MethodsDnet.add ty id !meth_dnet
 
-let in_method =
+let in_method : constr * MethodsDnet.ident -> obj =
   declare_object
     { (default_object "RECMETHODS") with
 	load_function = (fun _ -> load_method);
@@ -289,7 +295,7 @@ let subst_canonical_structure (subst,(cst,ind as obj)) =
 let discharge_canonical_structure (_,(cst,ind)) =
   Some (Lib.discharge_con cst,Lib.discharge_inductive ind)
 
-let inCanonStruc =
+let inCanonStruc : constant * inductive -> obj =
   declare_object {(default_object "CANONICAL-STRUCTURE") with
     open_function = open_canonical_structure;
     cache_function = cache_canonical_structure;