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/conv_oracle.ml | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'kernel/conv_oracle.ml')

diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 58668c0142..0851c7a5f9 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -45,14 +45,6 @@ let set_strategy k l =
       else Cmap.add c l !cst_opacity
   | RelKey _ -> Util.error "set_strategy: RelKey"
 
-let set_transparent_const kn =
-  cst_opacity := Cmap.remove kn !cst_opacity
-let set_transparent_var id =
-  var_opacity := Idmap.remove id !var_opacity
-
-let set_opaque_const kn = set_strategy (ConstKey kn) Opaque
-let set_opaque_var id = set_strategy (VarKey id) Opaque
-
 let get_transp_state () =
   (Idmap.fold
     (fun id l ts -> if  l=Opaque then Idpred.remove id ts else ts)
-- 
cgit v1.2.3