Removing dead code, thanks to new OCaml warnings and a bit of scripting.

6 files changed, 0 insertions, 29 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 104f26641..a7957ebe8 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -37,8 +37,6 @@ type pattern_matching_error =
   | BadConstructor of constructor * inductive
   | WrongNumargConstructor of constructor * int
   | WrongNumargInductive of inductive * int
-  | WrongPredicateArity of constr * constr * constr
-  | NeedsInversion of constr * constr
   | UnusedClause of cases_pattern list
   | NonExhaustive of cases_pattern list
   | CannotInferPredicate of (constr * types) array
@@ -60,12 +58,6 @@ let error_wrong_numarg_constructor_loc loc env c n =
 let error_wrong_numarg_inductive_loc loc env c n =
   raise_pattern_matching_error (loc, env, WrongNumargInductive(c,n))
 
-let error_wrong_predicate_arity_loc loc env c n1 n2 =
-  raise_pattern_matching_error (loc, env, WrongPredicateArity (c,n1,n2))
-
-let error_needs_inversion env x t =
-  raise (PatternMatchingError (env, NeedsInversion (x,t)))
-
 let rec list_try_compile f = function
   | [a] -> f a
   | [] -> anomaly (str "try_find_f")
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index b5bb27da9..70fa945ff 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -23,28 +23,16 @@ type pattern_matching_error =
   | BadConstructor of constructor * inductive
   | WrongNumargConstructor of constructor * int
   | WrongNumargInductive of inductive * int
-  | WrongPredicateArity of constr * constr * constr
-  | NeedsInversion of constr * constr
   | UnusedClause of cases_pattern list
   | NonExhaustive of cases_pattern list
   | CannotInferPredicate of (constr * types) array
 
 exception PatternMatchingError of env * pattern_matching_error
 
-val raise_pattern_matching_error : (Loc.t * env * pattern_matching_error) -> 'a
-
 val error_wrong_numarg_constructor_loc : Loc.t -> env -> constructor -> int -> 'a
 
 val error_wrong_numarg_inductive_loc : Loc.t -> env -> inductive -> int -> 'a
 
-val error_bad_constructor_loc : Loc.t -> constructor -> inductive -> 'a
-
-val error_bad_pattern_loc : Loc.t -> constructor -> constr -> 'a
-
-val error_wrong_predicate_arity_loc : Loc.t -> env -> constr -> constr -> constr -> 'a
-
-val error_needs_inversion : env -> constr -> types -> 'a
-
 (** {6 Compilation primitive. } *)
 
 val compile_cases :
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 170e21a90..c66ca7ac1 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -221,9 +221,6 @@ let get_type_of ?(polyprop=true) ?(refresh=true) ?(lax=false) env sigma c =
   let t = if lax then f env c else anomaly_on_error (f env) c in
   if refresh then refresh_universes t else t
 
-(* Makes an assumption from a constr *)
-let get_assumption_of env evc c = c
-
 (* Makes an unsafe judgment from a constr *)
 let get_judgment_of env evc c = { uj_val = c; uj_type = get_type_of env evc c }
 
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index bb3ffa411..c2a08f4b9 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -35,9 +35,6 @@ val get_sort_of :
 val get_sort_family_of :
   ?polyprop:bool -> env -> evar_map -> types -> sorts_family
 
-(** Makes an assumption from a constr *)
-val get_assumption_of : env -> evar_map -> constr -> types
-
 (** Makes an unsafe judgment from a constr *)
 val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index fbb7de7af..bfcc469c5 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1004,7 +1004,6 @@ let w_unify_core_0 env evd with_types cv_pb flags m n =
   let evd = w_merge env with_types flags subst2 in
   try_resolve_typeclasses env evd flags m n
 
-let w_unify_0 env evd = w_unify_core_0 env evd false
 let w_typed_unify env evd = w_unify_core_0 env evd true
 
 let w_typed_unify_array env evd flags f1 l1 f2 l2 =
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 5dd4587a0..04e65b862 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -60,8 +60,6 @@ val w_coerce_to_type : env -> evar_map -> constr -> types -> types ->
    (exported for inv.ml) *)
 val abstract_list_all :
   env -> evar_map -> constr -> constr -> constr list -> constr * types
-val abstract_list_all_with_dependencies :
-  env -> evar_map -> types -> constr -> constr list -> constr
 
 
 (* For tracing *)