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

7 files changed, 8 insertions, 177 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 8451d1285a..70b201a6e5 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -124,9 +124,6 @@ let make_anonymous_patvars n =
 (* Environment management *)
 let push_rels vars env = List.fold_right push_rel vars env
 
-let push_rel_defs =
-  List.fold_right (fun (x,d,t) e -> push_rel (x,Some d,t) e)
-
 (* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize
    over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *)
 
@@ -210,8 +207,6 @@ and pattern_continuation =
 
 let start_history n = Continuation (n, [], Top)
 
-let initial_history = function Continuation (_,[],Top) -> true | _ -> false
-
 let feed_history arg = function
   | Continuation (n, l, h) when n>=1 ->
       Continuation (n-1, arg :: l, h)
@@ -452,9 +447,6 @@ let map_tomatch_type f = function
 let liftn_tomatch_type n depth = map_tomatch_type (liftn n depth)
 let lift_tomatch_type n = liftn_tomatch_type n 1
 
-let lift_tomatch n ((current,typ),info) =
-  ((lift n current,lift_tomatch_type n typ),info)
-
 (**********************************************************************)
 (* Utilities on patterns *)
 
@@ -467,12 +459,6 @@ let alias_of_pat = function
   | PatVar (_,name) -> name
   | PatCstr(_,_,_,name) -> name
 
-let unalias_pat = function
-  | PatVar (c,name) as p ->
-      if name = Anonymous then p else PatVar (c,Anonymous)
-  | PatCstr(a,b,c,name) as p ->
-      if name = Anonymous then p else PatCstr (a,b,c,Anonymous)
-
 let remove_current_pattern eqn =
   match eqn.patterns with
     | pat::pats ->
@@ -658,9 +644,6 @@ let replace_tomatch n c =
       :: replrec (depth+1) rest in
   replrec 0
 
-let liftn_rel_declaration n k = map_rel_declaration (liftn n k)
-let substnl_rel_declaration sigma k = map_rel_declaration (substnl sigma k)
-
 let rec liftn_tomatch_stack n depth = function
   | [] -> []
   | Pushed ((c,tm),l,dep)::rest ->
@@ -1283,102 +1266,6 @@ let matx_of_eqns env tomatchl eqns =
       rhs = rhs }
   in List.map build_eqn eqns
 
-(************************************************************************)
-(* preparing the elimination predicate if any                          *)
-
-let build_expected_arity env evdref isdep tomatchl =
-  let cook n = function
-    | _,IsInd (_,IndType(indf,_),_) ->
-        let indf' = lift_inductive_family n indf in
-	Some (build_dependent_inductive env indf', fst (get_arity env indf'))
-    | _,NotInd _ -> None
-  in
-  let rec buildrec n env = function
-    | [] -> new_Type ()
-    | tm::ltm ->
-	match cook n tm with
-	  | None -> buildrec n env ltm
-	  | Some (ty1,aritysign) ->
-	      let rec follow n env = function
-		| d::sign ->
-		    mkProd_or_LetIn_name env
-		      (follow (n+1) (push_rel d env) sign) d
-		| [] ->
-		    if isdep then
-		      mkProd (Anonymous, ty1, 
-			      buildrec (n+1)
-				(push_rel_assum (Anonymous, ty1) env)
-				ltm)
-		    else buildrec n env ltm
-	      in follow n env (List.rev aritysign)
-  in buildrec 0 env tomatchl
-
-let extract_predicate_conclusion isdep tomatchl pred =
-  let cook = function
-    | _,IsInd (_,IndType(_,args),_) -> Some (List.length args)
-    | _,NotInd _ -> None in
-  let rec decomp_lam_force n l p =
-    if n=0 then (l,p) else
-    match kind_of_term p with
-      | Lambda (na,_,c) -> decomp_lam_force (n-1) (na::l) c
-      | _ -> (* eta-expansion *)
-          let na = Name (id_of_string "x") in
-          decomp_lam_force (n-1) (na::l) (applist (lift 1 p, [mkRel 1])) in
-  let rec buildrec allnames p = function
-    | [] -> (List.rev allnames,p)
-    | tm::ltm ->
-	match cook tm with
-	  | None -> 
-              let p = 
-                (* adjust to a sign containing the NotInd's *)
-                if isdep then lift 1 p else p in
-              let names = if isdep then [Anonymous] else [] in
-              buildrec (names::allnames) p ltm
-	  | Some n ->
-              let n = if isdep then n+1 else n in
-              let names,p = decomp_lam_force n [] p in
-              buildrec (names::allnames) p ltm
-  in buildrec [] pred tomatchl
-
-let set_arity_signature dep n arsign tomatchl pred x =
-  (* avoid is not exhaustive ! *)
-  let rec decomp_lam_force n avoid l p =
-    if n = 0 then (List.rev l,p,avoid) else
-    match p with
-      | RLambda (_,(Name id as na),_,_,c) -> 
-          decomp_lam_force (n-1) (id::avoid) (na::l) c
-      | RLambda (_,(Anonymous as na),_,_,c) -> decomp_lam_force (n-1) avoid (na::l) c
-      | _ ->
-          let x = next_ident_away (id_of_string "x") avoid in
-          decomp_lam_force (n-1) (x::avoid) (Name x :: l) 
-          (* eta-expansion *)
-            (let a = RVar (dummy_loc,x) in
-             match p with
-               | RApp (loc,p,l) -> RApp (loc,p,l@[a])
-               | _ -> (RApp (dummy_loc,p,[a]))) in
-  let rec decomp_block avoid p = function
-    | ([], _) -> x := Some p
-    | ((_,IsInd (_,IndType(indf,realargs),_))::l),(y::l')  ->
-	let (ind,params) = dest_ind_family indf in
-        let (nal,p,avoid') = decomp_lam_force (List.length realargs) avoid [] p 
-        in
-        let na,p,avoid' = 
-          if dep then decomp_lam_force 1 avoid' [] p else [Anonymous],p,avoid'
-        in 
-        y :=
-        (List.hd na,
-         if List.for_all ((=) Anonymous) nal then
-           None
-         else
-           Some (dummy_loc, ind, (List.map (fun _ -> Anonymous) params)@nal));
-        decomp_block avoid' p (l,l')
-    | (_::l),(y::l') ->
-        y := (Anonymous,None);
-        decomp_block avoid p (l,l')
-    | _ -> anomaly "set_arity_signature"
-  in
-  decomp_block [] pred (tomatchl,arsign)
-
 (***************** Building an inversion predicate ************************)
 
 (* Let "match t1 in I1 u11..u1n_1 ... tm in Im um1..umn_m with ... end : T"
@@ -1754,11 +1641,6 @@ let prepare_predicate_from_arsign_tycon loc env tomatchs sign arsign c =
  * tycon to make the predicate if it is not closed.
  *)
 
-let is_dependent_on_rel x t =
-  match kind_of_term x with
-      Rel n -> not (noccur_with_meta n n t)
-    | _ -> false
-
 let prepare_predicate loc typing_fun evdref env tomatchs sign tycon pred =
   match pred with
   (* No type annotation *)
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
 
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 69b5db5e63..576e217aa5 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -32,7 +32,6 @@ open Coercion.Default
 
 let pf_env gls = Global.env_of_context gls.it.evar_hyps
 let pf_type_of gls c  = Typing.type_of (pf_env gls) gls.sigma c
-let pf_hnf_constr gls c = hnf_constr (pf_env gls) gls.sigma c
 let pf_concl gl = gl.it.evar_concl
 
 (******************************************************************)
@@ -167,8 +166,6 @@ let mentions clenv mv0 =
     meta_exists menrec mlist
   in menrec
 
-let clenv_defined clenv mv = meta_defined clenv.evd mv
-
 let error_incompatible_inst clenv mv  =
   let na = meta_name clenv.evd mv in
   match na with
@@ -197,8 +194,6 @@ let clenv_assign mv rhs clenv =
     error "clenv_assign: undefined meta"
 
 
-let clenv_wtactic f clenv = {clenv with evd = f clenv.evd }
-
 
 (* [clenv_dependent hyps_only clenv]
  * returns a list of the metavars which appear in the template of clenv,
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 3a5f351255..f8545fdc95 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -73,11 +73,6 @@ module Default = struct
   (* Typing operations dealing with coercions *)
   exception NoCoercion
 
-  let whd_app_evar sigma t =
-    match kind_of_term t with
-      | App (f,l) -> mkApp (whd_evar sigma f,l)
-      | _ -> whd_evar sigma t
-
   (* Here, funj is a coercion therefore already typed in global context *)
   let apply_coercion_args env argl funj =
     let rec apply_rec acc typ = function
@@ -156,7 +151,6 @@ module Default = struct
 	    inh_tosort_force loc env evd j
 
   let inh_coerce_to_base loc env evd j = (evd, j)
-
   let inh_coerce_to_prod loc env evd t = (evd, t)
 
   let inh_coerce_to_fail env evd rigidonly v t c1 =
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index d455ec6fe5..1a7bb2c6cf 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -261,10 +261,6 @@ let e_new_evar evdref env ?(src=(dummy_loc,InternalHole)) ?filter ty =
  * operations on the evar constraints *
  *------------------------------------*)
 
-let is_pattern inst =
-  array_for_all (fun a -> isRel a || isVar a) inst &&
-  array_distinct inst
-
 (* Pb: defined Rels and Vars should not be considered as a pattern... *)
 (*
 let is_pattern inst =
@@ -275,19 +271,6 @@ let is_pattern inst =
   is_hopat [] (Array.to_list inst)
 *)
 
-let evar_well_typed_body evd ev evi body =
-  try
-    let env = evar_unfiltered_env evi in
-    let ty = evi.evar_concl in
-    Typing.check env ( evd) body ty;
-    true
-  with e ->
-    pperrnl
-      (str "Ill-typed evar instantiation: " ++ fnl() ++
-       pr_evar_defs evd ++ fnl() ++
-       str "----> " ++ int ev ++ str " := " ++
-       print_constr body);
-    false
 
 (* We have x1..xq |- ?e1 and had to solve something like 
  * Σ; Γ |- ?e1[u1..uq] = (...\y1 ... \yk ... c), where c is typically some 
@@ -807,12 +790,6 @@ let solve_evar_evar f env evd ev1 ev2 =
   with CannotProject projs2 ->
   postpone_evar_evar env evd projs1 ev1 projs2 ev2
 
-let expand_rhs env sigma subst rhs =
-  let d = (named_hd env rhs Anonymous,Some rhs,get_type_of env sigma rhs) in
-  let rhs' = lift 1 rhs in
-  let f (id,(idc,t)) = (id,(idc,replace_term rhs' (mkRel 1) (lift 1 t))) in
-  push_rel d env, List.map f subst, mkRel 1
-
 (* We try to instantiate the evar assuming the body won't depend
  * on arguments that are not Rels or Vars, or appearing several times
  * (i.e. we tackle a generalization of Miller-Pfenning patterns unification) 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 0f2f4655b9..500e190020 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -177,11 +177,8 @@ type sort_constraint =
   | SortVar of sort_var list * sort_var list (* (leq,geq) *)
   | EqSort of sort_var
 
-module UniverseOrdered = struct
-  type t = Univ.universe
-  let compare = Pervasives.compare
-end
-module UniverseMap = Map.Make(UniverseOrdered)
+module UniverseMap =
+  Map.Make (struct type t = Univ.universe let compare = compare end)
 
 type sort_constraints = sort_constraint UniverseMap.t
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index d3bbce9e31..55df4b185e 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