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

4 files changed, 19 insertions, 8 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index f6eaaa6656..03ae6e763a 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -405,7 +405,10 @@ let discharge_coercion (_,(coe,stre,isid,cls,clt,ps)) =
 let classify_coercion (coe,stre,isid,cls,clt,ps as obj) =
   if stre = Local then Dispose else Substitute obj
 
-let inCoercion =
+type coercion_obj =
+  coe_typ * Decl_kinds.locality * bool * cl_typ * cl_typ * int
+
+let inCoercion : coercion_obj -> obj =
   declare_object {(default_object "COERCION") with
     open_function = open_coercion;
     load_function = load_coercion;
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 0f1b9ac970..994fe33d09 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;
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index e5b94449ca..b4e76756bb 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -25,8 +25,10 @@ type struc_typ = {
   s_PROJKIND : (name * bool) list;
   s_PROJ : constant option list }
 
-val declare_structure :
-  inductive * constructor * (name * bool) list * constant option list -> unit
+type struc_tuple =
+    inductive * constructor * (name * bool) list * constant option list
+
+val declare_structure : struc_tuple -> unit
 
 (** [lookup_structure isp] returns the struc_typ associated to the
    inductive path [isp] if it corresponds to a structure, otherwise
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index caee039e0e..89e0fc93d7 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -210,7 +210,7 @@ let rebuild_class cl =
       set_typeclass_transparency cst false false; cl
   with _ -> cl
 
-let class_input =
+let class_input : typeclass -> obj =
   declare_object
     { (default_object "type classes state") with
       cache_function = cache_class;
@@ -282,7 +282,7 @@ let load_instance (_, (action, inst) as ai) =
   if action = AddInstance then
     add_instance_hint inst.is_impl (is_local inst) inst.is_pri
 
-let instance_input =
+let instance_input : instance_action * instance -> obj =
   declare_object
     { (default_object "type classes instances state") with
       cache_function = cache_instance;