diff options
| author | Pierre-Marie Pédrot | 2014-04-22 15:31:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-04-23 12:09:14 +0200 |
| commit | 74ddca99c649f2f8c203582a9b82bddf64fb6b52 (patch) | |
| tree | f23aa6340c2630619864666ef5eed257d3d765d9 /pretyping/cases.ml | |
| parent | d23c7539887366202bc370d0f80c26a557486e1c (diff) | |
Removing dead code, thanks to new OCaml warnings and a bit of scripting.
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 104f266419..a7957ebe84 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") |