From b359ef0ffad7fd1fc0e4db99fc1e38a1389802bc Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 2 Nov 2011 18:59:57 +0000
Subject: 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
---
 interp/implicit_quantifiers.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'interp/implicit_quantifiers.ml')

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))
 
-- 
cgit v1.2.3