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
---
 proofs/redexpr.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'proofs/redexpr.ml')

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index c6b3339d72..0430a239e2 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);
-- 
cgit v1.2.3