diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-24 13:14:17 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-24 13:14:17 +0000 |
| commit | c789e243ff599db876e94a5ab2a13ff98baa0d6c (patch) | |
| tree | 6dffe51299d60f2fb9ad8fa0a90c5b8a2cd119d9 /pretyping/recordops.ml | |
| parent | 61222d6bfb2fddd8608bea4056af2e9541819510 (diff) | |
Some dead code removal, thanks to Oug analyzer
In particular, the unused lib/tlm.ml and lib/gset.ml are removed
In addition, to simplify code, Libobject.record_object returning only the
('a->obj) function, which is enough almost all the time.
Use Libobject.record_object_full if you really need also the (obj->'a).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/recordops.ml')
| -rw-r--r-- | pretyping/recordops.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index f75f4990a..d477ec34a 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -76,7 +76,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,outStruc) = +let inStruc = declare_object {(default_object "STRUCTURE") with cache_function = cache_structure; load_function = load_structure; @@ -135,7 +135,7 @@ open Libobject let load_method (_,(ty,id)) = meth_dnet := MethodsDnet.add ty id !meth_dnet -let (in_method,out_method) = +let in_method = declare_object { (default_object "RECMETHODS") with load_function = (fun _ -> load_method); @@ -290,7 +290,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,outCanonStruct) = +let inCanonStruc = declare_object {(default_object "CANONICAL-STRUCTURE") with open_function = open_canonical_structure; cache_function = cache_canonical_structure; @@ -328,8 +328,6 @@ let check_and_decompose_canonical_structure ref = let declare_canonical_structure ref = add_canonical_structure (check_and_decompose_canonical_structure ref) -let outCanonicalStructure x = fst (outCanonStruct x) - let lookup_canonical_conversion (proj,pat) = List.assoc pat (Refmap.find proj !object_table) |