diff options
| author | letouzey | 2010-09-24 13:14:17 +0000 |
|---|---|---|
| committer | letouzey | 2010-09-24 13:14:17 +0000 |
| commit | c789e243ff599db876e94a5ab2a13ff98baa0d6c (patch) | |
| tree | 6dffe51299d60f2fb9ad8fa0a90c5b8a2cd119d9 /pretyping/typeclasses.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/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 15 |
1 files changed, 2 insertions, 13 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index b381f295c4..b1cbed4afb 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -32,10 +32,6 @@ let register_set_typeclass_transparency = (:=) set_typeclass_transparency_ref let set_typeclass_transparency gr c = !set_typeclass_transparency_ref gr c -let mismatched_params env n m = mismatched_ctx_inst env Parameters n m -(* let mismatched_defs env n m = mismatched_ctx_inst env Definitions n m *) -let mismatched_props env n m = mismatched_ctx_inst env Properties n m - type rels = constr list (* This module defines type-classes *) @@ -197,7 +193,7 @@ let discharge_class (_,cl) = let rebuild_class cl = cl -let (class_input,class_output) = +let class_input = declare_object { (default_object "type classes state") with cache_function = cache_class; @@ -246,7 +242,7 @@ let classify_instance inst = if inst.is_global = -1 then Dispose else Substitute inst -let (instance_input,instance_output) = +let instance_input = declare_object { (default_object "type classes instances state") with cache_function = cache_instance; @@ -304,13 +300,6 @@ let instance_constructor cl args = let typeclasses () = Gmap.fold (fun _ l c -> l :: c) !classes [] -let cmapl_add x y m = - try - let l = Gmap.find x m in - Gmap.add x (Gmap.add y.is_impl y l) m - with Not_found -> - Gmap.add x (Gmap.add y.is_impl y Gmap.empty) m - let cmap_elements c = Gmap.fold (fun k v acc -> v :: acc) c [] let instances_of c = |