diff options
| author | Hugo Herbelin | 2020-04-13 00:50:06 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-12-09 11:04:47 +0100 |
| commit | c8c93bfea6e3c75ebce256f44043a34fe8933b5e (patch) | |
| tree | 264633478d3dff7b3777f57311024aad83090237 /pretyping/cases.mli | |
| parent | 3f286f3fcb846cac360969372d71e91c5aefe810 (diff) | |
Fixing support for argument scopes and let-ins while interning cases patterns.
We also simplify the whole process of interpretation of cases pattern
on the way.
Diffstat (limited to 'pretyping/cases.mli')
| -rw-r--r-- | pretyping/cases.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 9a986bc14c..10fd085e3a 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -23,17 +23,17 @@ open Evardefine type pattern_matching_error = | BadPattern of constructor * constr | BadConstructor of constructor * inductive - | WrongNumargConstructor of constructor * int - | WrongNumargInductive of inductive * int + | WrongNumargConstructor of constructor * bool * int * int * int + | WrongNumargInductive of inductive * bool * int * int * int | UnusedClause of cases_pattern list | NonExhaustive of cases_pattern list | CannotInferPredicate of (constr * types) array exception PatternMatchingError of env * evar_map * pattern_matching_error -val error_wrong_numarg_constructor : ?loc:Loc.t -> env -> constructor -> int -> 'a +val error_wrong_numarg_constructor : ?loc:Loc.t -> env -> constructor -> bool -> int -> int -> int -> 'a -val error_wrong_numarg_inductive : ?loc:Loc.t -> env -> inductive -> int -> 'a +val error_wrong_numarg_inductive : ?loc:Loc.t -> env -> inductive -> bool -> int -> int -> int -> 'a val irrefutable : env -> cases_pattern -> bool |