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

1 files changed, 6 insertions, 2 deletions

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;