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, 11 insertions, 7 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index a104cd5db4..f273904353 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -56,14 +56,14 @@ let cache_generalizable_type (_,(local,cmd)) =
 
 let load_generalizable_type _ (_,(local,cmd)) =
   generalizable_table := add_generalizable cmd !generalizable_table
-    
-let in_generalizable =
+
+let in_generalizable : bool * identifier located list option -> obj =
   declare_object {(default_object "GENERALIZED-IDENT") with
     load_function = load_generalizable_type;
     cache_function = cache_generalizable_type;
     classify_function = (fun (local, _ as obj) -> if local then Dispose else Keep obj)
   }
-    
+
 let declare_generalizable local gen =
  Lib.add_anonymous_leaf (in_generalizable (local, gen))
 
diff --git a/interp/notation.ml b/interp/notation.ml
index ae14cd5ca9..aa35e4af08 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -117,7 +117,7 @@ let discharge_scope (_,(local,_,_ as o)) =
 let classify_scope (local,_,_ as o) =
   if local then Dispose else Substitute o
 
-let inScope =
+let inScope : bool * bool * scope_elem -> obj =
   declare_object {(default_object "SCOPE") with
       cache_function = cache_scope;
       open_function = open_scope;
@@ -520,7 +520,11 @@ let rebuild_arguments_scope (req,r,l,_) =
 	let l1,_ = list_chop (List.length l' - List.length l) l' in
 	(req,r,l1@l,cls)
 
-let inArgumentsScope =
+type arguments_scope_obj =
+    arguments_scope_discharge_request * global_reference *
+      scope_name option list * Classops.cl_typ option list
+
+let inArgumentsScope : arguments_scope_obj -> obj =
   declare_object {(default_object "ARGUMENTS-SCOPE") with
       cache_function = cache_arguments_scope;
       load_function = load_arguments_scope;
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 6c96e20c16..a07f5c8463 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -37,7 +37,7 @@ let cache_reserved_type (_,(id,t)) =
   reserve_table := Idmap.add id t !reserve_table;
   reserve_revtable := Gmapl.add key (t,id) !reserve_revtable
 
-let in_reserved =
+let in_reserved : identifier * aconstr -> obj =
   declare_object {(default_object "RESERVED-TYPE") with
     cache_function = cache_reserved_type }
 
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 8056ab426e..8863bbbd3b 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -62,7 +62,7 @@ let subst_syntax_constant (subst,(local,pat,onlyparse)) =
 let classify_syntax_constant (local,_,_ as o) =
   if local then Dispose else Substitute o
 
-let in_syntax_constant =
+let in_syntax_constant : bool * interpretation * bool -> obj =
   declare_object {(default_object "SYNTAXCONSTANT") with
     cache_function = cache_syntax_constant;
     load_function = load_syntax_constant;