Remove some dead-code (thanks to ocaml warnings)

 The removed code isn't used locally and isn't exported in the signature

4 files changed, 2 insertions, 43 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index bdc4bc0ae..a96adcdd8 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -768,10 +768,6 @@ let filter_candidates evd evk filter candidates =
       let ids = set_of_evctx (Filter.filter_list filter (evar_context evi)) in
       Some (List.filter (fun a -> Id.Set.subset (collect_vars a) ids) l)
 
-let eq_filter f1 f2 =
-  let eq_bool b1 b2 = if b1 then b2 else not b2 in
-  List.equal eq_bool f1 f2
-
 let closure_of_filter evd evk = function
   | None -> None
   | Some filter ->
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 49ce29fdf..21a418943 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -176,41 +176,6 @@ let new_meta =
 
 let mk_new_meta () = mkMeta(new_meta())
 
-(** Transfer an evar from [sigma2] to [sigma1] *)
-let transfer ev (sigma1, sigma2) =
-  let nsigma1 = Evd.add sigma1 ev (Evd.find sigma2 ev) in
-  let nsigma2 = Evd.remove sigma2 ev in
-  (nsigma1, nsigma2)
-
-let collect_evars emap c =
-  let rec collrec acc c =
-    match kind_of_term c with
-      | Evar (evk,_) ->
-	  if Evd.is_undefined emap evk then Evar.Set.add evk acc
-	  else (* No recursion on the evar instantiation *) acc
-      | _         ->
-	  fold_constr collrec acc c in
-  collrec Evar.Set.empty c
-
-let push_dependent_evars sigma emap =
-  let fold ev {evar_concl = ccl} (sigma, emap) =
-    Evar.Set.fold transfer (collect_evars emap ccl) (sigma, emap)
-  in
-  Evd.fold_undefined fold emap (sigma, emap)
-
-let push_duplicated_evars sigma emap c =
-  let rec collrec (one, evars as acc) c =
-    match kind_of_term c with
-    | Evar (evk,_) when not (Evd.mem (fst evars) evk) ->
-	if List.exists (fun ev -> Evar.equal evk ev) one then
-	  (one, transfer evk evars)
-	else
-	  (evk::one, evars)
-    | _ ->
-	fold_constr collrec acc c
-  in
-  snd (collrec ([],(sigma,emap)) c)
-
 (* The list of non-instantiated existential declarations (order is important) *)
 
 let non_instantiated sigma =
@@ -221,8 +186,6 @@ let non_instantiated sigma =
 (* Manipulating filters *)
 (************************)
 
-let extract_subfilter = List.filter_with
-
 let make_pure_subst evi args =
   snd (List.fold_right
     (fun (id,b,c) (args,l) ->
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index cf08e6787..0b6c3197d 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -492,7 +492,7 @@ let apply_subst recfun env cst_l t stack =
     | _ -> recfun cst_l (substl env t, stack)
   in aux env cst_l t stack
 
-let rec stacklam recfun env t stack =
+let stacklam recfun env t stack =
 apply_subst (fun _ -> recfun) env [] t stack
 
 let beta_applist (c,l) =
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index a6a9a75c5..b16f000d4 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -48,7 +48,7 @@ let unsatisfiable_constraints env evd ev comp =
 
 let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))
 
-let rec unsatisfiable_exception exn =
+let unsatisfiable_exception exn =
   match exn with
   | TypeClassError (_, UnsatisfiableConstraints _) -> true
   | _ -> false