diff options
| author | Hugo Herbelin | 2020-12-02 17:22:16 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-12-09 11:04:47 +0100 |
| commit | dc7a4f056d97c43badaa6ca5901eafb951527d88 (patch) | |
| tree | 699360da8a42aa36faab86139b9dd64c138c8ade /vernac | |
| parent | a33172c4f781f7ea2e7420aad9ffb5cfe077d66d (diff) | |
Using self-documenting argument names in two exceptions of cases.ml.
Namely, WrongNumargInductive and WrongNumargConstructor.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index a38dfdb419..bff0359782 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1371,10 +1371,10 @@ let explain_pattern_matching_error env sigma = function explain_bad_pattern env sigma c t | BadConstructor (c,ind) -> explain_bad_constructor env c ind - | WrongNumargConstructor (c,expanded,n,n1,n2) -> - explain_wrong_numarg_constructor env c expanded n n1 n2 - | WrongNumargInductive (c,expanded,n,n1,n2) -> - explain_wrong_numarg_inductive env c expanded n n1 n2 + | WrongNumargConstructor {cstr; expanded; nargs; expected_nassums; expected_ndecls} -> + explain_wrong_numarg_constructor env cstr expanded nargs expected_nassums expected_ndecls + | WrongNumargInductive {ind; expanded; nargs; expected_nassums; expected_ndecls} -> + explain_wrong_numarg_inductive env ind expanded nargs expected_nassums expected_ndecls | UnusedClause tms -> explain_unused_clause env tms | NonExhaustive tms -> |