diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 21 | ||||
| -rw-r--r-- | pretyping/cases.mli | 12 |
2 files changed, 21 insertions, 12 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 14417d15c6..d2859b1b4e 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -46,8 +46,10 @@ module NamedDecl = Context.Named.Declaration type pattern_matching_error = | BadPattern of constructor * constr | BadConstructor of constructor * inductive - | WrongNumargConstructor of constructor * bool * int * int * int - | WrongNumargInductive of inductive * bool * int * int * int + | WrongNumargConstructor of + {cstr:constructor; expanded:bool; nargs:int; expected_nassums:int; expected_ndecls:int} + | WrongNumargInductive of + {ind:inductive; expanded:bool; nargs:int; expected_nassums:int; expected_ndecls:int} | UnusedClause of cases_pattern list | NonExhaustive of cases_pattern list | CannotInferPredicate of (constr * types) array @@ -65,11 +67,13 @@ let error_bad_constructor ?loc env cstr ind = raise_pattern_matching_error ?loc (env, Evd.empty, BadConstructor (cstr,ind)) -let error_wrong_numarg_constructor ?loc env c expanded n n1 n2 = - raise_pattern_matching_error ?loc (env, Evd.empty, WrongNumargConstructor(c,expanded,n,n1,n2)) +let error_wrong_numarg_constructor ?loc env ~cstr ~expanded ~nargs ~expected_nassums ~expected_ndecls = + raise_pattern_matching_error ?loc (env, Evd.empty, + WrongNumargConstructor {cstr; expanded; nargs; expected_nassums; expected_ndecls}) -let error_wrong_numarg_inductive ?loc env c expanded n n1 n2 = - raise_pattern_matching_error ?loc (env, Evd.empty, WrongNumargInductive(c,expanded,n,n1,n2)) +let error_wrong_numarg_inductive ?loc env ~ind ~expanded ~nargs ~expected_nassums ~expected_ndecls = + raise_pattern_matching_error ?loc (env, Evd.empty, + WrongNumargInductive {ind; expanded; nargs; expected_nassums; expected_ndecls}) let list_try_compile f l = let rec aux errors = function @@ -528,8 +532,9 @@ let check_and_adjust_constructor env ind cstrs pat = match DAst.get pat with with NotAdjustable -> let nlet = List.count (function LocalDef _ -> true | _ -> false) ci.cs_args in (* In practice, this is already checked at interning *) - error_wrong_numarg_constructor ?loc env cstr - (* as if not expanded: *) false nargs nb_args_constr (nb_args_constr + nlet) + error_wrong_numarg_constructor ?loc env ~cstr + (* as if not expanded: *) ~expanded:false ~nargs ~expected_nassums:nb_args_constr + ~expected_ndecls:(nb_args_constr + nlet) else (* Try to insert a coercion *) try diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 10fd085e3a..ade1fbf3d3 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -23,17 +23,21 @@ open Evardefine type pattern_matching_error = | BadPattern of constructor * constr | BadConstructor of constructor * inductive - | WrongNumargConstructor of constructor * bool * int * int * int - | WrongNumargInductive of inductive * bool * int * int * int + | WrongNumargConstructor of + {cstr:constructor; expanded:bool; nargs:int; expected_nassums:int; expected_ndecls:int} + | WrongNumargInductive of + {ind:inductive; expanded:bool; nargs:int; expected_nassums:int; expected_ndecls: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 -> bool -> int -> int -> int -> 'a +val error_wrong_numarg_constructor : + ?loc:Loc.t -> env -> cstr:constructor -> expanded:bool -> nargs:int -> expected_nassums:int -> expected_ndecls:int -> 'a -val error_wrong_numarg_inductive : ?loc:Loc.t -> env -> inductive -> bool -> int -> int -> int -> 'a +val error_wrong_numarg_inductive : + ?loc:Loc.t -> env -> ind:inductive -> expanded:bool -> nargs:int -> expected_nassums:int -> expected_ndecls:int -> 'a val irrefutable : env -> cases_pattern -> bool |