From f8b5525eea31c226dfb2ebdc22be512f8af2ebbe Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 8 Apr 2009 17:23:13 +0000 Subject: 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 --- kernel/retroknowledge.ml | 18 ++++-------------- 1 file changed, 4 insertions(+), 14 deletions(-) (limited to 'kernel/retroknowledge.ml') diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index 44f5dcb32..44d13a0cb 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -77,14 +77,9 @@ type flags = {fastcomputation : bool} (*A definition of maps from strings to pro_int31, to be able to have any amount of coq representation for the 31bits integers *) -module OrderedField = -struct - type t = field - let compare = compare -end - -module Proactive = Map.Make (OrderedField) +module Proactive = + Map.Make (struct type t = field let compare = compare end) type proactive = entry Proactive.t @@ -98,13 +93,8 @@ type proactive = entry Proactive.t a finite type describing the fields to the field of proactive retroknowledge (and then to make as many functions as needed in environ.ml) *) -module OrderedEntry = -struct - type t = entry - let compare = compare -end - -module Reactive = Map.Make (OrderedEntry) +module Reactive = + Map.Make (struct type t = entry let compare = compare end) type reactive_end = {(*information required by the compiler of the VM *) vm_compiling : -- cgit v1.2.3