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

6 files changed, 8 insertions, 6 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 8fc403b78b..72917530b2 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -487,6 +487,8 @@ type hint_action =
   | AddHints of hint_entry list
   | RemoveHints of global_reference list
 
+type hint_obj = bool * string * hint_action  (* locality, name, action *)
+
 let cache_autohint (_,(local,name,hints)) =
   match hints with
   | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty st b)
@@ -556,7 +558,7 @@ let subst_autohint (subst,(local,name,hintlist as obj)) =
 let classify_autohint ((local,name,hintlist) as obj) =
   if local or hintlist = (AddHints []) then Dispose else Substitute obj
 
-let inAutoHint =
+let inAutoHint : hint_obj -> obj =
   declare_object {(default_object "AUTOHINT") with
                     cache_function = cache_autohint;
 		    load_function = (fun _ -> cache_autohint);
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 13f8784f58..c9951bea2d 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -223,7 +223,7 @@ let classify_hintrewrite x = Libobject.Substitute x
 
 
 (* Declaration of the Hint Rewrite library object *)
-let inHintRewrite =
+let inHintRewrite : string * HintDN.t -> Libobject.obj =
   Libobject.declare_object {(Libobject.default_object "HINT_REWRITE") with
     Libobject.cache_function = cache_hintrewrite;
     Libobject.load_function = (fun _ -> cache_hintrewrite);
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index f9c316955c..fd924707c8 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -220,7 +220,7 @@ let subst_dd (subst,(local,na,dd)) =
     d_pri = dd.d_pri;
     d_code = !forward_subst_tactic subst dd.d_code })
 
-let inDD =
+let inDD : bool * identifier * destructor_data -> obj =
   declare_object {(default_object "DESTRUCT-HYP-CONCL-DATA") with
                     cache_function = cache_dd;
 		    open_function = (fun i o -> if i=1 then cache_dd o);
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 4af1bce7de..bae28c7ce8 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -442,7 +442,7 @@ let cache_transitivity_lemma (_,(left,lem)) =
 
 let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref)
 
-let inTransitivity =
+let inTransitivity : bool * constr -> obj =
   declare_object {(default_object "TRANSITIVITY-STEPS") with
     cache_function = cache_transitivity_lemma;
     open_function = (fun i o -> if i=1 then cache_transitivity_lemma o);
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index b310dd6451..90e4582fa7 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2844,7 +2844,7 @@ let subst_md (subst,(local,defs)) =
 let classify_md (local,defs as o) =
   if local then Dispose else Substitute o
 
-let inMD =
+let inMD : bool * (tacdef_kind * glob_tactic_expr) list -> obj =
   declare_object {(default_object "TAC-DEFINITION") with
      cache_function  = cache_md;
      load_function   = load_md;
diff --git a/tactics/tactic_option.ml b/tactics/tactic_option.ml
index 1310fe7f9c..57b8c54067 100644
--- a/tactics/tactic_option.ml
+++ b/tactics/tactic_option.ml
@@ -25,7 +25,7 @@ let declare_tactic_option ?(default=Tacexpr.TacId []) name =
   let subst (s, (local, tac)) =
     (local, Tacinterp.subst_tactic s tac)
   in
-  let input =
+  let input : bool * Tacexpr.glob_tactic_expr -> obj =
     declare_object
       { (default_object name) with
 	cache_function = cache;