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 --- pretyping/recordops.ml | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) (limited to 'pretyping/recordops.ml') 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; -- cgit v1.2.3