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

1 files changed, 5 insertions, 12 deletions

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index d3bbce9e3..55df4b185 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -109,19 +109,12 @@ type constant_evaluation =
 
 (* We use a cache registered as a global table *)
 
-module CstOrdered =
-  struct
-    type t = constant
-    let compare = Pervasives.compare
-  end
-module Cstmap = Map.Make(CstOrdered)
+let eval_table = ref Cmap.empty
 
-let eval_table = ref Cstmap.empty
-
-type frozen = (int * constant_evaluation) Cstmap.t
+type frozen = (int * constant_evaluation) Cmap.t
 
 let init () =
-  eval_table := Cstmap.empty
+  eval_table := Cmap.empty
 
 let freeze () =
   !eval_table
@@ -272,10 +265,10 @@ let compute_consteval sigma env ref =
 let reference_eval sigma env = function
   | EvalConst cst as ref -> 
       (try
-	 Cstmap.find cst !eval_table
+	 Cmap.find cst !eval_table
        with Not_found -> begin
 	 let v = compute_consteval sigma env ref in
-	 eval_table := Cstmap.add cst v !eval_table;
+	 eval_table := Cmap.add cst v !eval_table;
 	 v
        end)
   | ref -> compute_consteval sigma env ref