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

8 files changed, 26 insertions, 88 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 10ef06993..c4759fa92 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -379,9 +379,6 @@ let rec decomp_stack = function
         | _ ->
             Some (v.(0), (Zapp (Array.sub v 1 (Array.length v - 1)) :: s)))
   | _ -> None
-let rec decomp_stackn = function
-  | Zapp v :: s -> if Array.length v = 0 then decomp_stackn s else (v, s)
-  | _ -> assert false
 let array_of_stack s =
   let rec stackrec = function
   | [] -> []
@@ -430,8 +427,6 @@ let lift_fconstr k f =
   if k=0 then f else lft_fconstr k f
 let lift_fconstr_vect k v =
   if k=0 then v else Array.map (fun f -> lft_fconstr k f) v
-let lift_fconstr_list k l =
-  if k=0 then l else List.map (fun f -> lft_fconstr k f) l
 
 let clos_rel e i =
   match expand_rel i e with
@@ -741,12 +736,6 @@ let get_nth_arg head n stk =
 
 (* Beta reduction: look for an applied argument in the stack.
    Since the encountered update marks are removed, h must be a whnf *)
-let get_arg h stk =
-  let (depth,stk') = strip_update_shift h stk in
-  match  decomp_stack stk' with
-      Some (v, s') -> (Some (depth,v), s')
-    | None -> (None, zshift depth stk')
-
 let rec get_args n tys f e stk =
   match stk with
       Zupdate r :: s ->
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 58668c014..0851c7a5f 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)
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 8dde8fb3e..e30fe7737 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -70,14 +70,7 @@ type constant_entry =
 
 (*s Modules *)
 
-type specification_entry = 
-    SPEconst of constant_entry
-  | SPEmind of mutual_inductive_entry
-  | SPEmodule of module_entry
-  | SPEalias of module_path
-  | SPEmodtype of module_struct_entry
-
-and module_struct_entry = 
+type module_struct_entry = 
     MSEident of module_path
   | MSEfunctor of mod_bound_id * module_struct_entry * module_struct_entry
   | MSEwith of module_struct_entry * with_declaration
@@ -87,8 +80,6 @@ and with_declaration =
     With_Module of identifier list * module_path
   | With_Definition of identifier list * constr
 
-and module_structure = (label * specification_entry) list
-
 and module_entry = 
     { mod_entry_type : module_struct_entry option;
       mod_entry_expr : module_struct_entry option}
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 6de90d29c..dc1522dbf 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -69,14 +69,7 @@ type constant_entry =
 
 (*s Modules *)
 
-type specification_entry = 
-    SPEconst of constant_entry
-  | SPEmind of mutual_inductive_entry
-  | SPEmodule of module_entry
-  | SPEalias of module_path
-  | SPEmodtype of module_struct_entry
-
-and module_struct_entry = 
+type module_struct_entry =
     MSEident of module_path
   | MSEfunctor of mod_bound_id * module_struct_entry * module_struct_entry
   | MSEwith of module_struct_entry * with_declaration
@@ -86,8 +79,6 @@ and with_declaration =
     With_Module of identifier list * module_path
   | With_Definition of identifier list * constr
 
-and module_structure = (label * specification_entry) list
-
 and module_entry = 
     { mod_entry_type : module_struct_entry option;
       mod_entry_expr : module_struct_entry option}
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 4fb5a2b1a..e0f364f2e 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -60,12 +60,6 @@ let push_rel_context ctxt x = Sign.fold_rel_context push_rel ctxt ~init:x
 let push_rec_types (lna,typarray,_) env =
   let ctxt = array_map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
   Array.fold_left (fun e assum -> push_rel assum e) env ctxt
-    
-let reset_rel_context env =
-  { env with
-    env_rel_context = empty_rel_context;
-    env_rel_val = [];
-    env_nb_rel = 0 }
 
 let fold_rel_context f env ~init =
   let rec fold_right env =
diff --git a/kernel/names.ml b/kernel/names.ml
index 6ee96fddd..953c13aa9 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -51,13 +51,7 @@ type name = Name of identifier | Anonymous
 type module_ident = identifier
 type dir_path = module_ident list
 
-module ModIdOrdered = 
-  struct
-    type t = identifier
-    let compare = Pervasives.compare
-  end
-
-module ModIdmap = Map.Make(ModIdOrdered)
+module ModIdmap = Idmap
 
 let make_dirpath x = x
 let repr_dirpath x = x
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 :
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 65fc78203..24af5da05 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -55,19 +55,17 @@ let cmp_univ_level u v = match u,v with
       else if i1 > i2 then 1
       else compare dp1 dp2
 
-type universe =
-  | Atom of universe_level
-  | Max of universe_level list * universe_level list
-  
-module UniverseOrdered = struct
-  type t = universe_level
-  let compare = cmp_univ_level
-end
-
 let string_of_univ_level = function
   | Set -> "0"
   | Level (d,n) -> Names.string_of_dirpath d^"."^string_of_int n
 
+module UniverseLMap =
+ Map.Make (struct type t = universe_level let compare = cmp_univ_level end)
+
+type universe =
+  | Atom of universe_level
+  | Max of universe_level list * universe_level list
+
 let make_univ (m,n) = Atom (Level (m,n))
 
 let pr_uni_level u = str (string_of_univ_level u)
@@ -121,18 +119,17 @@ type univ_entry =
     Canonical of canonical_arc
   | Equiv of universe_level * universe_level
 
-module UniverseMap = Map.Make(UniverseOrdered)
 
-type universes = univ_entry UniverseMap.t
-		   
+type universes = univ_entry UniverseLMap.t
+
 let enter_equiv_arc u v g =
-  UniverseMap.add u (Equiv(u,v)) g
+  UniverseLMap.add u (Equiv(u,v)) g
 
 let enter_arc ca g =
-  UniverseMap.add ca.univ (Canonical ca) g
+  UniverseLMap.add ca.univ (Canonical ca) g
 
 let declare_univ u g =
-  if not (UniverseMap.mem u g) then
+  if not (UniverseLMap.mem u g) then
     enter_arc (terminal u) g
   else
     g
@@ -162,7 +159,7 @@ let is_univ_variable = function
 
 let type1_univ = Max ([],[Set])
 
-let initial_universes = UniverseMap.empty
+let initial_universes = UniverseLMap.empty
 
 (* Every universe_level has a unique canonical arc representative *)
 
@@ -171,7 +168,7 @@ let initial_universes = UniverseMap.empty
 let repr g u = 
   let rec repr_rec u =
     let a =
-      try UniverseMap.find u g
+      try UniverseLMap.find u g
       with Not_found -> anomalylabstrm "Univ.repr"
 	  (str"Universe " ++ pr_uni_level u ++ str" undefined") 
     in
@@ -443,7 +440,7 @@ let enforce_univ_relation g = function
 (* Merging 2 universe graphs *)
 (*
 let merge_universes sp u1 u2 =
-  UniverseMap.fold (fun _ a g -> enforce_univ_relation g a) u1 u2
+  UniverseLMap.fold (fun _ a g -> enforce_univ_relation g a) u1 u2
 *)
 
 
@@ -571,14 +568,14 @@ let no_upper_constraints u cst =
 (* Pretty-printing *)
 
 let num_universes g =
-  UniverseMap.fold (fun _ _ -> succ) g 0
+  UniverseLMap.fold (fun _ _ -> succ) g 0
 
 let num_edges g =
   let reln_len = function
     | Equiv _ -> 1
     | Canonical {lt=lt;le=le} -> List.length lt + List.length le
   in
-  UniverseMap.fold (fun _ a n -> n + (reln_len a)) g 0
+  UniverseLMap.fold (fun _ a n -> n + (reln_len a)) g 0
     
 let pr_arc = function 
   | Canonical {univ=u; lt=[]; le=[]} ->
@@ -594,7 +591,7 @@ let pr_arc = function
       pr_uni_level u  ++ str " = " ++ pr_uni_level v ++ fnl ()
 
 let pr_universes g =
-  let graph = UniverseMap.fold (fun k a l -> (k,a)::l) g [] in
+  let graph = UniverseLMap.fold (fun k a l -> (k,a)::l) g [] in
   prlist (function (_,a) -> pr_arc a) graph
     
 let pr_constraints c =
@@ -626,7 +623,7 @@ let dump_universes output g =
 	Printf.fprintf output "%s = %s ;\n"
 	  (string_of_univ_level u) (string_of_univ_level v)
   in
-    UniverseMap.iter dump_arc g 
+    UniverseLMap.iter dump_arc g 
 
 (* Hash-consing *)