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