Remove some more "open" and dead code thanks to OCaml4 warnings

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7

13 files changed, 3 insertions, 103 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index b6b8f8dba..7b6be410b 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -62,15 +62,6 @@ let error_wrong_predicate_arity_loc loc env c n1 n2 =
 let error_needs_inversion env x t =
   raise (PatternMatchingError (env, NeedsInversion (x,t)))
 
-module type S = sig
-  val compile_cases :
-    Loc.t -> case_style ->
-    (type_constraint -> env -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref ->
-    type_constraint ->
-    env -> glob_constr option * tomatch_tuples * cases_clauses ->
-    unsafe_judgment
-end
-
 let rec list_try_compile f = function
   | [a] -> f a
   | [] -> anomaly "try_find_f"
@@ -396,10 +387,6 @@ let type_of_tomatch = function
   | IsInd (t,_,_) -> t
   | NotInd (_,t) -> t
 
-let mkDeclTomatch na = function
-  | IsInd (t,_,_) -> (na,None,t)
-  | NotInd (c,t) -> (na,c,t)
-
 let map_tomatch_type f = function
   | IsInd (t,ind,names) -> IsInd (f t,map_inductive_type f ind,names)
   | NotInd (c,t) -> NotInd (Option.map f c, f t)
@@ -1800,8 +1787,6 @@ let string_of_name name =
     | Anonymous -> "anonymous"
     | Name n -> string_of_id n
 
-let id_of_name n = id_of_string (string_of_name n)
-
 let make_prime_id name =
   let str = string_of_name name in
     id_of_string str, id_of_string (str ^ "'")
@@ -1981,22 +1966,6 @@ let build_ineqs prevpatterns pats liftsign =
   in match diffs with [] -> None
     | _ -> Some (mk_coq_and diffs)
 
-let subst_rel_context k ctx subst =
-  let (_, ctx') =
-    List.fold_right
-      (fun (n, b, t) (k, acc) ->
-	 (succ k, (n, Option.map (substnl subst k) b, substnl subst k t) :: acc))
-      ctx (k, [])
-  in ctx'
-
-let lift_rel_contextn n k sign =
-  let rec liftrec k = function
-    | (na,c,t)::sign ->
-	(na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
-    | [] -> []
-  in
-  liftrec (rel_context_length sign + k) sign
-
 let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity =
   let i = ref 0 in
   let (x, y, z) =
@@ -2111,10 +2080,6 @@ let abstract_tomatch env tomatchs tycon =
       ([], [], [], tycon) tomatchs
   in List.rev prev, ctx, tycon
 
-let is_dependent_ind = function
-    IsInd (_, IndType (indf, args), _) when List.length args > 0 -> true
-  | _ -> false
-
 let build_dependent_signature env evars avoid tomatchs arsign =
   let avoid = ref avoid in
   let arsign = List.rev arsign in
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 14476354b..52ec8d1d1 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -406,10 +406,7 @@ let discharge_coercion (_,(coe,stre,isid,cls,clt,ps)) =
 let classify_coercion (coe,stre,isid,cls,clt,ps as obj) =
   if stre = Local then Dispose else Substitute obj
 
-type coercion_obj =
-  coe_typ * Decl_kinds.locality * bool * cl_typ * cl_typ * int
-
-let inCoercion : coercion_obj -> obj =
+let inCoercion : coercion -> obj =
   declare_object {(default_object "COERCION") with
     open_function = open_coercion;
     load_function = load_coercion;
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f931d723f..30f6de5c2 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -582,10 +582,6 @@ let filter_possible_projections c ty ctxt args =
     Idset.mem id tyvars)
     ctxt args
 
-let initial_evar_data evi =
-  let ids = List.map pi1 (evar_context evi) in
-  (evar_filter evi, List.map mkVar ids)
-
 let solve_evars = ref (fun _ -> failwith "solve_evars not installed")
 let set_solve_evars f = solve_evars := f
 
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index e51415abb..45df12e46 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1126,16 +1126,6 @@ let invert_arg evd aliases k evk subst_in_env_extended_with_k_binders c_in_env_e
   | _ ->
       res
 
-let effective_projections =
-  List.map_filter (function Invertible c -> Some c | _ -> None)
-
-let instance_of_projection f env t evd projs =
-  let ty = lazy (nf_evar evd (Retyping.get_type_of env evd t)) in
-  match projs with
-  | NoUniqueProjection -> raise NotUnique
-  | UniqueProjection (c,effects) ->
-      (List.fold_left (do_projection_effects f env ty) evd effects, c)
-
 exception NotEnoughInformationToInvert
 
 let extract_unique_projections projs =
@@ -1157,8 +1147,6 @@ let extract_candidates sols =
   with Exit ->
     None
 
-let filter_of_projection = function Invertible _ -> true | _ -> false
-
 let invert_invertible_arg evd aliases k (evk,argsv) args' =
   let evi = Evd.find_undefined evd evk in
   let subst,_ = make_projectable_subst aliases evd evi argsv in
@@ -1899,7 +1887,6 @@ let check_evars env initial_sigma sigma c =
       | _ -> iter_constr proc_rec c
   in proc_rec c
 
-
 (****************************************)
 (* Operations on value/type constraints *)
 (****************************************)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 1394f3ba8..cc6bd6150 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -672,10 +672,6 @@ let retract_coercible_metas evd =
       evd.metas ([],Metamap.empty) in
   mc, { evd with metas = ml }
 
-let rec list_assoc_in_triple x = function
-    [] -> raise Not_found
-  | (a,b,_)::l -> if compare a x = 0 then b else list_assoc_in_triple x l
-
 let subst_defined_metas bl c =
   let rec substrec c = match kind_of_term c with
     | Meta i -> substrec (List.assoc_snd_in_triple i bl)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index ed65cc9ea..8c216d99b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -158,13 +158,6 @@ let evd_comb2 f evdref x y =
     evdref := evd';
     z
 
-let evd_comb3 f evdref x y z =
-  let (evd',t) = f !evdref x y z in
-    evdref := evd';
-    t
-
-let mt_evd = Evd.empty
-
 (* Utilisé pour inférer le prédicat des Cases *)
 (* Semble exagérement fort *)
 (* Faudra préférer une unification entre les types de toutes les clauses *)
@@ -256,8 +249,6 @@ let pretype_sort evdref = function
   | GSet -> judge_of_set
   | GType _ -> evd_comb0 judge_of_new_Type evdref
 
-exception Found of fixpoint
-
 let new_type_evar evdref env loc =
   evd_comb0 (fun evd -> Evarutil.new_type_evar evd env ~src:(loc,Evar_kinds.InternalHole)) evdref
 
diff --git a/pretyping/program.ml b/pretyping/program.ml
index db821f176..a8e91856b 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -11,8 +11,6 @@ open Util
 open Names
 open Term
 
-type message = string
-
 let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
 
 let find_reference locstr dir s =
@@ -63,10 +61,3 @@ let mk_coq_and l =
       (fun c conj ->
 	 mkApp (and_typ, [| c ; conj |]))
       l
-
-let with_program f c = 
-  let mode = !Flags.program_mode in
-    Flags.program_mode := true;
-    let res = f c in
-      Flags.program_mode := mode;
-      res
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index f20c0dd83..b417dc1d4 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -907,8 +907,6 @@ let whd_programs_stack env sigma =
 let whd_programs env sigma x =
   zip (whd_programs_stack env sigma (x, empty_stack))
 
-exception IsType
-
 let find_conclusion env sigma =
   let rec decrec env c =
     let t = whd_betadeltaiota env sigma c in
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 3563e9ca2..97ce40a77 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -124,9 +124,9 @@ type constant_evaluation =
 
 (* We use a cache registered as a global table *)
 
-let eval_table = ref Cmap.empty
+type frozen = constant_evaluation Cmap.t
 
-type frozen = (int * constant_evaluation) Cmap.t
+let eval_table = ref (Cmap.empty : frozen)
 
 let init () =
   eval_table := Cmap.empty
diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml
index 451dde11f..8372d31da 100644
--- a/pretyping/term_dnet.ml
+++ b/pretyping/term_dnet.ml
@@ -48,8 +48,6 @@ struct
     | DCons   of ('t * 't option) * 't
     | DNil
 
-  type dconstr = dconstr t
-
   (* debug *)
   let pr_dconstr f : 'a t -> std_ppcmds = function
     | DRel -> str "*"
@@ -203,11 +201,6 @@ struct
 
   type ident = TDnet.ident
 
-  type 'a pattern = 'a TDnet.pattern
-  type term_pattern = term_pattern DTerm.t pattern
-
-  type idset = TDnet.Idset.t
-
   type result = ident * (constr*existential_key) * Termops.subst
 
   open DTerm
@@ -268,10 +261,6 @@ struct
     let c = empty_ctx (pat_of_constr c) in
     TDnet.add dn c id
 
-  let new_meta_no =
-    let ctr = ref 0 in
-    fun () -> decr ctr; !ctr
-
   let new_meta_no = Evarutil.new_untyped_evar
 
   let neutral_meta = new_meta_no()
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 426197af2..2749538c0 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -44,7 +44,6 @@ let solve_instanciation_problem = ref (fun _ _ _ -> assert false)
 let resolve_one_typeclass env evm t =
   !solve_instanciation_problem env evm t
 
-type rels = constr list
 type direction = Forward | Backward
 
 (* This module defines type-classes *)
@@ -327,11 +326,6 @@ let classify_instance (action, inst) =
   if is_local inst then Dispose
   else Substitute (action, inst)
 
-let load_instance (_, (action, inst) as ai) =
-  cache_instance ai;
-  if action = AddInstance then
-    add_instance_hint (constr_of_global inst.is_impl) (is_local inst) inst.is_pri
-
 let instance_input : instance_action * instance -> obj =
   declare_object
     { (default_object "type classes instances state") with
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 053c1cd7b..4a0b66a7b 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -12,7 +12,6 @@ open Term
 open Evd
 open Environ
 open Constrexpr
-open Util
 open Globnames
 (*i*)
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 8955cc64c..886c4a3aa 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -313,9 +313,6 @@ let elim_no_delta_flags = {
   allow_K_in_toplevel_higher_order_unification = true
 }
 
-let set_no_head_reduction flags =
-  { flags with restrict_conv_on_strict_subterms = true }
-
 let use_evars_pattern_unification flags =
   !global_evars_pattern_unification_flag && flags.use_pattern_unification
   && Flags.version_strictly_greater Flags.V8_2