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, 23 insertions, 8 deletions

diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index bb5ab795d4..30c537f282 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -51,7 +51,7 @@ let discharge_scheme (_,(kind,l)) =
   Some (kind,Array.map (fun (ind,const) ->
     (Lib.discharge_inductive ind,Lib.discharge_con const)) l)
 
-let inScheme =
+let inScheme : string * (inductive * constant) array -> obj =
   declare_object {(default_object "SCHEME") with
                     cache_function = cache_scheme;
                     load_function = (fun _ -> cache_scheme);
diff --git a/toplevel/libtypes.ml b/toplevel/libtypes.ml
index c182fb3854..2f98962cf4 100644
--- a/toplevel/libtypes.ml
+++ b/toplevel/libtypes.ml
@@ -71,7 +71,7 @@ let subst a b = Profile.profile2 subst_key TypeDnet.subst a b
 let load_key = Profile.declare_profile "load"
 let load a = Profile.profile1 load_key load a
 *)
-let input =
+let input : TypeDnet.t -> obj =
   declare_object
     { (default_object "LIBTYPES") with
 	load_function = (fun _ -> load);
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 3c7e98722f..6a4d72516a 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -32,7 +32,7 @@ open Nameops
 
 let cache_token (_,s) = add_keyword s
 
-let inToken =
+let inToken : string -> obj =
   declare_object {(default_object "TOKEN") with
        open_function = (fun i o -> if i=1 then cache_token o);
        cache_function = cache_token;
@@ -70,7 +70,12 @@ let subst_tactic_parule subst (key,n,p,(d,tac)) =
 let subst_tactic_notation (subst,(pa,pp)) =
   (subst_tactic_parule subst pa,pp)
 
-let inTacticGrammar =
+type tactic_grammar_obj =
+    (string * int * grammar_prod_item list *
+       (dir_path * Tacexpr.glob_tactic_expr))
+    * (string * Genarg.argument_type list * (int * Pptactic.grammar_terminals))
+
+let inTacticGrammar : tactic_grammar_obj -> obj =
   declare_object {(default_object "TacticGrammar") with
        open_function = (fun i o -> if i=1 then cache_tactic_notation o);
        cache_function = cache_tactic_notation;
@@ -710,7 +715,13 @@ let subst_syntax_extension (subst,(local,sy)) =
 let classify_syntax_definition (local,_ as o) =
   if local then Dispose else Substitute o
 
-let inSyntaxExtension =
+type syntax_extension_obj =
+    bool *
+      (notation_var_internalization_type list * Notation.level *
+         notation * notation_grammar * unparsing list)
+      list
+
+let inSyntaxExtension : syntax_extension_obj -> obj =
   declare_object {(default_object "SYNTAX-EXTENSION") with
        open_function = (fun i o -> if i=1 then cache_syntax_extension o);
        cache_function = cache_syntax_extension;
@@ -962,7 +973,11 @@ let subst_notation (subst,(lc,scope,pat,b,ndf)) =
 let classify_notation (local,_,_,_,_ as o) =
   if local then Dispose else Substitute o
 
-let inNotation =
+type notation_obj =
+    bool * scope_name option * interpretation * bool *
+      (notation * notation_location)
+
+let inNotation : notation_obj -> obj =
   declare_object {(default_object "NOTATION") with
        open_function = open_notation;
        cache_function = cache_notation;
@@ -1138,7 +1153,7 @@ let subst_scope_command (subst,(scope,o as x)) = match o with
       scope, ScopeClasses cl'
   | _ -> x
 
-let inScopeCommand =
+let inScopeCommand : scope_name * scope_command -> obj =
   declare_object {(default_object "DELIMITERS") with
       cache_function = cache_scope_command;
       open_function = open_scope_command;
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index d9a261ed46..3cda904258 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -296,7 +296,7 @@ let cache_ml_module_object (_,{mnames=mnames}) =
 let classify_ml_module_object ({mlocal=mlocal} as o) =
   if mlocal then Dispose else Substitute o
 
-let inMLModule =
+let inMLModule : ml_module_object -> obj =
   declare_object {(default_object "ML-MODULE") with
                     load_function = (fun _ -> cache_ml_module_object);
                     cache_function = cache_ml_module_object;