diff options
| author | letouzey | 2009-04-08 17:23:13 +0000 |
|---|---|---|
| committer | letouzey | 2009-04-08 17:23:13 +0000 |
| commit | f8b5525eea31c226dfb2ebdc22be512f8af2ebbe (patch) | |
| tree | 2e3783d78cb21cd4e5b5cbbfe02ecfce40acc959 /pretyping/classops.ml | |
| parent | e285c447b9bc478f9c9fc7b2459a7e9a11b5358c (diff) | |
Some dead code removal + cleanups
This commit concerns about the first half of the useless code
mentionned by Oug for coqtop (without plugins). For the moment,
Oug is used in a mode where any elements mentionned in a .mli
is considered to be precious. This already allows to detect and
remove about 600 lines, and more is still to come.
Among the interesting points, the type Entries.specification_entry
and its constructors SPExxx were never used. Large parts of cases.ml
(and hence subtac_cases.ml) were also useless.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12069 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/classops.ml')
| -rw-r--r-- | pretyping/classops.ml | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index b0554540af..11d6ed093a 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -68,8 +68,6 @@ module Bijint = struct (let v = Array.make (b.s + 8) (x,y) in Array.blit b.v 0 v 0 b.s; v) else b.v in v.(b.s) <- (x,y); { v = v; s = b.s+1; inv = Gmap.add x b.s b.inv } - let replace n x y b = - let v = Array.copy b.v in v.(n) <- (x,y); { b with v = v } let dom b = Gmap.dom b.inv end @@ -138,8 +136,6 @@ let coercion_info coe = Gmap.find coe !coercion_tab let coercion_exists coe = Gmap.mem coe !coercion_tab -let coercion_params coe_info = coe_info.coe_param - (* find_class_type : env -> evar_map -> constr -> cl_typ * int *) let find_class_type env sigma t = @@ -383,7 +379,7 @@ let discharge_coercion (_,(coe,stre,isid,cls,clt,ps)) = discharge_cl clt, n + ps) -let (inCoercion,outCoercion) = +let (inCoercion,_) = declare_object {(default_object "COERCION") with load_function = load_coercion; cache_function = cache_coercion; @@ -395,9 +391,6 @@ let (inCoercion,outCoercion) = let declare_coercion coef stre ~isid ~src:cls ~target:clt ~params:ps = Lib.add_anonymous_leaf (inCoercion (coef,stre,isid,cls,clt,ps)) -let coercion_strength v = v.coe_strength -let coercion_identity v = v.coe_is_identity - (* For printing purpose *) let get_coercion_value v = v.coe_value |