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

33 files changed, 180 insertions, 142 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index a104cd5db..f27390435 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 ae14cd5ca..aa35e4af0 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 6c96e20c1..a07f5c846 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 8056ab426..8863bbbd3 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;
diff --git a/library/declare.ml b/library/declare.ml
index 10dc35b95..0afd4bd9e 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -78,7 +78,10 @@ let discharge_variable (_,o) = match o with
   | Inr (id,_) -> Some (Inl (variable_constraints id))
   | Inl _ -> Some o
 
-let inVariable =
+type variable_obj =
+    (Univ.constraints, identifier * variable_declaration) union
+
+let inVariable : variable_obj -> obj =
   declare_object { (default_object "VARIABLE") with
     cache_function = cache_variable;
     discharge_function = discharge_variable;
@@ -151,7 +154,10 @@ let dummy_constant (ce,_,mk) = dummy_constant_entry,[],mk
 
 let classify_constant cst = Substitute (dummy_constant cst)
 
-let inConstant =
+type constant_obj =
+    global_declaration * Dischargedhypsmap.discharged_hyps * logical_kind
+
+let inConstant : constant_obj -> obj =
   declare_object { (default_object "CONSTANT") with
     cache_function = cache_constant;
     load_function = load_constant;
@@ -246,7 +252,9 @@ let dummy_inductive_entry (_,m) = ([],{
   mind_entry_finite = true;
   mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds })
 
-let inInductive =
+type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry
+
+let inInductive : inductive_obj -> obj =
   declare_object {(default_object "INDUCTIVE") with
     cache_function = cache_inductive;
     load_function = load_inductive;
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 95d2310ce..90d4245a4 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -179,14 +179,21 @@ let check_sub mtb sub_mtb_l =
    environment. *)
 
 let check_subtypes mp sub_mtb_l =
-  let mb = Global.lookup_module mp in
+  let mb =
+    try Global.lookup_module mp
+    with Not_found -> assert false
+  in
   let mtb = Modops.module_type_of_module None mb in
   check_sub mtb sub_mtb_l
 
 (* Same for module type [mp] *)
 
 let check_subtypes_mt mp sub_mtb_l =
-  check_sub (Global.lookup_modtype mp) sub_mtb_l
+  let mtb =
+    try Global.lookup_modtype mp
+    with Not_found -> assert false
+  in
+  check_sub mtb sub_mtb_l
 
 (* Create a functor type entry *)
 
@@ -274,42 +281,26 @@ let conv_names_do_module exists what iter_objects i
    functions can be called only once (and "end_mod*" set the flag to
    false then)
 *)
-let cache_module ((sp,kn),(entry,substobjs)) =
+let cache_module ((sp,kn),substobjs) =
   let dir,mp = dir_of_sp sp, mp_of_kn kn in
     do_module false "cache" load_objects 1 dir mp substobjs []
-    
-(* TODO: This check is not essential *)
-let check_empty s = function
-     | None -> ()
-     | Some _ ->
-	 anomaly ("We should never have full info in " ^ s^"!")
-
 
 (* When this function is called the module itself is already in the
    environment. This function loads its objects only *)
 
-let load_module i (oname,(entry,substobjs)) =
-  (* TODO: This check is not essential *)
-  check_empty "load_module" entry;
+let load_module i (oname,substobjs) =
   conv_names_do_module false "load" load_objects i oname substobjs
 
-
-let open_module i (oname,(entry,substobjs)) =
-  (* TODO: This check is not essential *)
-  check_empty "open_module" entry;
+let open_module i (oname,substobjs) =
   conv_names_do_module true "open" open_objects i oname substobjs
 
+let subst_module (subst,(mbids,mp,objs)) =
+  (mbids,subst_mp subst mp, subst_objects subst objs)
 
+let classify_module substobjs = Substitute substobjs
 
-let subst_module (subst,(entry,(mbids,mp,objs))) =
-  check_empty "subst_module" entry;
-    (None,(mbids,subst_mp subst mp, subst_objects subst objs))
-
-
-let classify_module (_,substobjs) =
-  Substitute (None,substobjs)
-
-let (in_module,out_module) =
+let (in_module : substitutive_objects -> obj),
+    (out_module : obj -> substitutive_objects) =
   declare_object_full {(default_object "MODULE") with
     cache_function = cache_module;
     load_function = load_module;
@@ -337,7 +328,7 @@ let open_keep i ((sp,kn),seg) =
   let dirpath,mp = dir_of_sp sp, mp_of_kn kn in
     open_objects i (dirpath,(mp,empty_dirpath)) seg
 
-let in_modkeep =
+let in_modkeep : lib_objects -> obj =
   declare_object {(default_object "MODULE KEEP OBJECTS") with
     cache_function = cache_keep;
     load_function = load_keep;
@@ -369,6 +360,7 @@ let _ = Summary.declare_summary "MODTYPE-INFO"
 let cache_modtype ((sp,kn),(entry,modtypeobjs,sub_mty_l)) =
   let mp = mp_of_kn kn in
 
+  (* We enrich the global environment *)
   let _ =
     match entry with
       | None ->
@@ -392,7 +384,7 @@ let cache_modtype ((sp,kn),(entry,modtypeobjs,sub_mty_l)) =
 
 
 let load_modtype i ((sp,kn),(entry,modtypeobjs,_)) =
-  check_empty "load_modtype" entry;
+  assert (entry = None);
 
   if Nametab.exists_modtype sp then
     errorlabstrm "cache_modtype"
@@ -404,7 +396,7 @@ let load_modtype i ((sp,kn),(entry,modtypeobjs,_)) =
 
 
 let open_modtype i ((sp,kn),(entry,_,_)) =
-  check_empty "open_modtype" entry;
+  assert (entry = None);
 
   if
     try Nametab.locate_modtype (qualid_of_path sp) <> (mp_of_kn kn)
@@ -416,15 +408,18 @@ let open_modtype i ((sp,kn),(entry,_,_)) =
   Nametab.push_modtype (Nametab.Exactly i) sp (mp_of_kn kn)
 
 let subst_modtype (subst,(entry,(mbids,mp,objs),_)) =
-  check_empty "subst_modtype" entry;
+  assert (entry = None);
   (entry,(mbids,subst_mp subst mp,subst_objects subst objs),[])
 
-
 let classify_modtype (_,substobjs,_) =
   Substitute (None,substobjs,[])
 
+type modtype_obj =
+    (module_struct_entry * Entries.inline) option (* will be None in vo *)
+    * substitutive_objects
+    * module_type_body list
 
-let in_modtype =
+let in_modtype : modtype_obj -> obj =
     declare_object {(default_object "MODULE TYPE") with
       cache_function = cache_modtype;
       open_function = open_modtype;
@@ -432,35 +427,27 @@ let in_modtype =
       subst_function = subst_modtype;
       classify_function = classify_modtype }
 
-let rec replace_module_object idl ( mbids, mp, lib_stack) (mbids2,mp2,objs) mp1=
-  if mbids<>[] then 
-    error "Unexpected functor objects"
-  else
-    let rec replace_idl = function 
-      | _,[] -> [] 
-      | id::idl,(id',obj)::tail when id = id' ->
-	  if object_tag obj = "MODULE" then
-           (match idl with
-               [] -> (id, in_module 
-			(None,(mbids,(MPdot(mp,label_of_id id)),subst_objects 
-				 (map_mp mp1 (MPdot(mp,label_of_id id)) empty_delta_resolver) objs)))::tail
-             | _ ->
-               let (_,substobjs) = out_module obj in
-                let substobjs' = replace_module_object idl substobjs 
-		  (mbids2,mp2,objs) mp in
-                  (id, in_module (None,substobjs'))::tail
-           )
-	  else error "MODULE expected!"
-      | idl,lobj::tail -> lobj::replace_idl (idl,tail)
-    in
-      (mbids, mp, replace_idl (idl,lib_stack))
+let rec replace_module_object idl (mbids,mp,lib_stack) (mbids2,mp2,objs) mp1 =
+  if mbids<>[] then anomaly "Unexpected functor objects";
+  let rec replace_idl = function
+    | _,[] -> []
+    | id::idl,(id',obj)::tail when id = id' ->
+      if object_tag obj <> "MODULE" then anomaly "MODULE expected!";
+      let substobjs =
+	if idl = [] then
+	  let mp' = MPdot(mp, label_of_id id) in
+	  mbids, mp', subst_objects (map_mp mp1 mp' empty_delta_resolver) objs
+	else
+	  replace_module_object idl (out_module obj) (mbids2,mp2,objs) mp
+      in
+      (id, in_module substobjs)::tail
+    | idl,lobj::tail -> lobj::replace_idl (idl,tail)
+  in
+  (mbids, mp, replace_idl (idl,lib_stack))
 
-let discr_resolver mb  = 
-     match mb.mod_type with
-	SEBstruct _ -> 
-	  Some mb.mod_delta
-      | _ -> (*case mp is a functor *)
-	  None
+let discr_resolver mb = match mb.mod_type with
+  | SEBstruct _ -> Some mb.mod_delta
+  | _ -> None (* when mp is a functor *)
 
 (* Small function to avoid module typing during substobjs retrivial  *)
 let rec get_objs_modtype_application env = function
@@ -622,7 +609,7 @@ let end_module () =
     | Some mp_from,(mbids,_,objs) ->
 	(mbids,mp,subst_objects (map_mp mp_from mp resolver) objs) 
   in
-  let node = in_module (None,substobjs) in
+  let node = in_module substobjs in
   let objects =
     if keep = [] || mbids <> [] then
       special@[node]   (* no keep objects or we are defining a functor *)
@@ -859,7 +846,7 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
   reset_scope_subst ();
   ignore (add_leaf
 	    id
-	    (in_module (Some (entry), substobjs)));
+	    (in_module substobjs));
   mmp
 
 (* Include *)
@@ -887,32 +874,33 @@ let lift_oname (sp,kn) =
   let dir,_ = Libnames.repr_path sp in
     (dir,mp)
 
-let cache_include (oname,((me,is_mod),(mbis,mp1,objs))) =
+let cache_include (oname,(me,(mbis,mp1,objs))) =
   let dir,mp1 = lift_oname oname in
   let prefix = (dir,(mp1,empty_dirpath)) in
     load_objects 1 prefix objs;
-    open_objects 1 prefix objs 
-    
-let load_include  i (oname,((me,is_mod),(mbis,mp1,objs))) =
+    open_objects 1 prefix objs
+
+let load_include  i (oname,(me,(mbis,mp1,objs))) =
   let dir,mp1 = lift_oname oname in
   let prefix = (dir,(mp1,empty_dirpath)) in
     load_objects i prefix objs
-      
-      
-let open_include i (oname,((me,is_mod),(mbis,mp1,objs))) =
+
+let open_include i (oname,(me,(mbis,mp1,objs))) =
   let dir,mp1 = lift_oname oname in
   let prefix = (dir,(mp1,empty_dirpath)) in
     open_objects i prefix objs
-          
-let subst_include (subst,((me,is_mod),substobj)) =
+
+let subst_include (subst,(me,substobj)) =
   let (mbids,mp,objs) = substobj in
   let substobjs = (mbids,subst_mp subst mp,subst_objects subst objs) in
-    ((subst_inc_expr subst me,is_mod),substobjs)
-      
-let classify_include ((me,is_mod),substobjs) =
-  Substitute ((me,is_mod),substobjs)
+    (subst_inc_expr subst me,substobjs)
+
+let classify_include (me,substobjs) = Substitute (me,substobjs)
+
+type include_obj = module_struct_entry * substitutive_objects
 
-let (in_include,out_include) =
+let (in_include : include_obj -> obj),
+    (out_include : obj -> include_obj) =
   declare_object_full {(default_object "INCLUDE") with
     cache_function = cache_include;
     load_function = load_include;
@@ -987,8 +975,7 @@ let declare_one_include_inner annot (me,is_mod) =
   let substobjs = (mbids,mp1,
 		   subst_objects (map_mp mp mp1 resolver) objs) in
   reset_scope_subst ();
-  ignore (add_leaf id
-	    (in_include ((me,is_mod), substobjs)))
+  ignore (add_leaf id (in_include (me, substobjs)))
 
 let declare_one_include interp_struct (me_ast,annot) =
   declare_one_include_inner annot
diff --git a/library/goptions.ml b/library/goptions.ml
index fbce68fad..7c522022f 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -94,7 +94,7 @@ module MakeTable =
 	    if p' == p then obj else
 	      (f,p')
 	in
-        let inGo =
+        let inGo : option_mark * A.t -> obj =
           Libobject.declare_object {(Libobject.default_object nick) with
                 Libobject.load_function = load_options;
 		Libobject.open_function = load_options;
diff --git a/library/heads.ml b/library/heads.ml
index 813031558..9f9f1ca25 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -167,7 +167,9 @@ let discharge_head (_,(ref,k)) =
 let rebuild_head (ref,k) =
   (ref, compute_head ref)
 
-let inHead =
+type head_obj = evaluable_global_reference * head_approximation
+
+let inHead : head_obj -> obj =
   declare_object {(default_object "HEAD") with
     cache_function = cache_head;
     load_function = load_head;
diff --git a/library/impargs.ml b/library/impargs.ml
index 3f60bf96a..2d5ffe9ab 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -548,7 +548,11 @@ let rebuild_implicits (req,l) =
 let classify_implicits (req,_ as obj) =
   if req = ImplLocal then Dispose else Substitute obj
 
-let inImplicits =
+type implicits_obj =
+    implicit_discharge_request *
+      (global_reference * implicits_list list) list
+
+let inImplicits : implicits_obj -> obj =
   declare_object {(default_object "IMPLICITS") with
     cache_function = cache_implicits;
     load_function = load_implicits;
diff --git a/library/lib.ml b/library/lib.ml
index 23d334a5d..7554fd0bb 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -539,7 +539,7 @@ let close_section () =
 (*****************)
 (* Backtracking. *)
 
-let (inLabel,outLabel) =
+let (inLabel : int -> obj), (outLabel : obj -> int) =
   declare_object_full {(default_object "DOT") with
 				classify_function = (fun _ -> Dispose)}
 
diff --git a/library/library.ml b/library/library.ml
index 9c602adbb..071c7a46c 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -300,7 +300,7 @@ let subst_import (_,o) = o
 let classify_import (_,export as obj) =
   if export then Substitute obj else Dispose
 
-let in_import =
+let in_import : dir_path * bool -> obj =
   declare_object {(default_object "IMPORT LIBRARY") with
        cache_function = cache_import;
        open_function = open_import;
@@ -498,7 +498,7 @@ let rec_intern_library_from_file idopt f =
 
 type library_reference = dir_path list * bool option
 
-let register_library (dir,m) =
+let register_library m =
   Declaremods.register_library
     m.library_name
     m.library_compiled
@@ -526,7 +526,9 @@ let discharge_require (_,o) = Some o
 
 (* open_function is never called from here because an Anticipate object *)
 
-let in_require =
+type require_obj = library_t list * dir_path list * bool option
+
+let in_require : require_obj -> obj =
   declare_object {(default_object "REQUIRE") with
        cache_function = cache_require;
        load_function = load_require;
@@ -541,7 +543,8 @@ let xml_require = ref (fun d -> ())
 let set_xml_require f = xml_require := f
 
 let require_library_from_dirpath modrefl export =
-  let needed = List.rev (List.fold_left rec_intern_library [] modrefl) in
+  let needed = List.fold_left rec_intern_library [] modrefl in
+  let needed = List.rev_map snd needed in
   let modrefl = List.map fst modrefl in
     if Lib.is_module_or_modtype () then
       begin
@@ -561,7 +564,7 @@ let require_library qidl export =
 
 let require_library_from_file idopt file export =
   let modref,needed = rec_intern_library_from_file idopt file in
-  let needed = List.rev needed in
+  let needed = List.rev_map snd needed in
   if Lib.is_module_or_modtype () then begin
     add_anonymous_leaf (in_require (needed,[modref],None));
     Option.iter (fun exp -> add_anonymous_leaf (in_import (modref,exp)))
diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml
index b025cea64..837195e44 100644
--- a/plugins/dp/dp.ml
+++ b/plugins/dp/dp.ml
@@ -36,7 +36,7 @@ let set_trace b = trace := b
 let timeout = ref 10
 let set_timeout n = timeout := n
 
-let dp_timeout_obj =
+let dp_timeout_obj : int -> obj =
   declare_object
     {(default_object "Dp_timeout") with
        cache_function = (fun (_,x) -> set_timeout x);
@@ -44,7 +44,7 @@ let dp_timeout_obj =
 
 let dp_timeout x = Lib.add_anonymous_leaf (dp_timeout_obj x)
 
-let dp_debug_obj =
+let dp_debug_obj : bool -> obj =
   declare_object
     {(default_object "Dp_debug") with
        cache_function = (fun (_,x) -> set_debug x);
@@ -52,7 +52,7 @@ let dp_debug_obj =
 
 let dp_debug x = Lib.add_anonymous_leaf (dp_debug_obj x)
 
-let dp_trace_obj =
+let dp_trace_obj : bool -> obj =
   declare_object
     {(default_object "Dp_trace") with
        cache_function = (fun (_,x) -> set_trace x);
@@ -825,7 +825,7 @@ let prelude_files = ref ([] : string list)
 
 let set_prelude l = prelude_files := l
 
-let dp_prelude_obj =
+let dp_prelude_obj : string list -> obj =
   declare_object
     {(default_object "Dp_prelude") with
        cache_function = (fun (_,x) -> set_prelude x);
@@ -1087,7 +1087,7 @@ let dp_hint l =
   in
   List.iter one_hint (List.map (fun qid -> qid, Nametab.global qid) l)
 
-let dp_hint_obj =
+let dp_hint_obj : reference list -> obj =
   declare_object
     {(default_object "Dp_hint") with
        cache_function = (fun (_,l) -> dp_hint l);
@@ -1113,7 +1113,7 @@ let dp_predefined qid s =
   with NotFO ->
     msg_warning (str " ignored (not a first order declaration)")
 
-let dp_predefined_obj =
+let dp_predefined_obj : reference * string -> obj =
   declare_object
     {(default_object "Dp_predefined") with
        cache_function = (fun (_,(id,s)) -> dp_predefined id s);
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 502d06235..75584ead3 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -493,7 +493,7 @@ let lang_ref = ref Ocaml
 
 let lang () = !lang_ref
 
-let extr_lang =
+let extr_lang : lang -> obj =
   declare_object
     {(default_object "Extraction Lang") with
        cache_function = (fun (_,l) -> lang_ref := l);
@@ -525,7 +525,7 @@ let add_inline_entries b l =
 
 (* Registration of operations for rollback. *)
 
-let inline_extraction =
+let inline_extraction : bool * global_reference list -> obj =
   declare_object
     {(default_object "Extraction Inline") with
        cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
@@ -569,7 +569,7 @@ let print_extraction_inline () =
 
 (* Reset part *)
 
-let reset_inline =
+let reset_inline : unit -> obj =
   declare_object
     {(default_object "Reset Extraction Inline") with
        cache_function = (fun (_,_)-> inline_table :=  empty_inline_table);
@@ -608,7 +608,7 @@ let add_implicits r l =
 
 (* Registration of operations for rollback. *)
 
-let implicit_extraction =
+let implicit_extraction : global_reference * int_or_id list -> obj =
   declare_object
     {(default_object "Extraction Implicit") with
        cache_function = (fun (_,(r,l)) -> add_implicits r l);
@@ -668,12 +668,11 @@ let add_blacklist_entries l =
 
 (* Registration of operations for rollback. *)
 
-let blacklist_extraction =
+let blacklist_extraction : string list -> obj =
   declare_object
     {(default_object "Extraction Blacklist") with
        cache_function = (fun (_,l) -> add_blacklist_entries l);
        load_function = (fun _ (_,l) -> add_blacklist_entries l);
-       classify_function = (fun o -> Libobject.Keep o);
        subst_function = (fun (_,x) -> x)
     }
 
@@ -696,7 +695,7 @@ let print_extraction_blacklist () =
 
 (* Reset part *)
 
-let reset_blacklist =
+let reset_blacklist : unit -> obj =
   declare_object
     {(default_object "Reset Extraction Blacklist") with
        cache_function = (fun (_,_)-> blacklist_table := Idset.empty);
@@ -742,7 +741,7 @@ let find_custom_match pv =
 
 (* Registration of operations for rollback. *)
 
-let in_customs =
+let in_customs : global_reference * string list * string -> obj =
   declare_object
     {(default_object "ML extractions") with
        cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s);
@@ -757,7 +756,7 @@ let _ = declare_summary "ML extractions"
 	    unfreeze_function = ((:=) customs);
 	    init_function = (fun () -> customs := Refmap'.empty) }
 
-let in_custom_matchs =
+let in_custom_matchs : global_reference * string -> obj =
   declare_object
     {(default_object "ML extractions custom matchs") with
        cache_function = (fun (_,(r,s)) -> add_custom_match r s);
diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4
index 8b6bb133a..9e4f4d745 100644
--- a/plugins/field/field.ml4
+++ b/plugins/field/field.ml4
@@ -67,7 +67,7 @@ let subst_addfield (subst,(typ,th as obj)) =
       (typ',th')
 
 (* Declaration of the Add Field library object *)
-let in_addfield =
+let in_addfield : types * constr -> Libobject.obj =
   Libobject.declare_object {(Libobject.default_object "ADD_FIELD") with
        Libobject.open_function = (fun i o -> if i=1 then cache_addfield o);
        Libobject.cache_function = cache_addfield;
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 094d2e50f..951b25baf 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -362,7 +362,7 @@ let pr_table tb =
   let l = Cmap.fold (fun k v acc -> v::acc) tb [] in
   Util.prlist_with_sep fnl pr_info l
 
-let in_Function =
+let in_Function : function_info -> Libobject.obj =
   Libobject.declare_object
     {(Libobject.default_object "FUNCTIONS_DB") with
        Libobject.cache_function = cache_Function;
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
index 9a252dfb7..98d6361c0 100644
--- a/plugins/ring/ring.ml
+++ b/plugins/ring/ring.ml
@@ -262,7 +262,7 @@ let subst_th (subst,(c,th as obj)) =
       (c',th')
 
 
-let theory_to_obj =
+let theory_to_obj : constr * theory -> obj =
   let cache_th (_,(c, th)) = theories_map_add (c,th) in
   declare_object {(default_object "tactic-ring-theory") with
 		    open_function = (fun i o -> if i=1 then cache_th o);
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 6ff673023..af236bc0f 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -438,7 +438,7 @@ let subst_th (subst,th) =
       ring_post_tac = posttac' }
 
 
-let theory_to_obj =
+let theory_to_obj : ring_info -> obj =
   let cache_th (name,th) = add_entry name th in
   declare_object
     {(default_object "tactic-new-ring-theory") with
@@ -1014,7 +1014,7 @@ let subst_th (subst,th) =
       field_pre_tac = pretac';
       field_post_tac = posttac' }
 
-let ftheory_to_obj =
+let ftheory_to_obj : field_info -> obj =
   let cache_th (name,th) = add_field_entry name th in
   declare_object
     {(default_object "tactic-new-field-theory") with
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index b3ff7c9f0..74ee05bbc 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -213,7 +213,7 @@ let close sec =
 			      (str (if List.length keys = 1 then " has " else "have ") ++
 			       str "unsolved obligations"))
 
-let input =
+let input : program_info ProgMap.t -> obj =
   declare_object
     { (default_object "Program state") with
       cache_function = (fun (na, pi) -> from_prg := pi);
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index f6eaaa665..03ae6e763 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 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;
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index e5b94449c..b4e76756b 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 caee039e0..89e0fc93d 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;
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index c6b3339d7..0430a239e 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -86,7 +86,10 @@ let discharge_strategy (_,(local,obj)) =
   if local then None else
   map_strategy disch_ref obj
 
-let inStrategy =
+type strategy_obj =
+    bool * (Conv_oracle.level * evaluable_global_reference list) list
+
+let inStrategy : strategy_obj -> obj =
   declare_object {(default_object "STRATEGY") with
                     cache_function = (fun (_,obj) -> cache_strategy obj);
 		    load_function = (fun _ (_,obj) -> cache_strategy obj);
@@ -212,7 +215,7 @@ let subst_red_expr subs e =
     (Pattern.subst_pattern subs)
     e
 
-let inReduction =
+let inReduction : bool * string * red_expr -> obj =
   declare_object
     {(default_object "REDUCTION") with
        cache_function = (fun (_,(_,s,e)) -> decl_red_expr s e);
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 8fc403b78..72917530b 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 13f8784f5..c9951bea2 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 f9c316955..fd924707c 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 4af1bce7d..bae28c7ce 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 b310dd645..90e4582fa 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 1310fe7f9..57b8c5406 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;
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index bb5ab795d..30c537f28 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 c182fb385..2f98962cf 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 3c7e98722..6a4d72516 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 d9a261ed4..3cda90425 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;