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 /interp | |
| parent | a33172c4f781f7ea2e7420aad9ffb5cfe077d66d (diff) | |
Using self-documenting argument names in two exceptions of cases.ml.
Namely, WrongNumargInductive and WrongNumargConstructor.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index f50521eb51..e3a4d1b169 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1426,8 +1426,8 @@ let check_has_letin ?loc g expanded nargs nimps tags = else if nargs = expected_ndecls then true else let env = Global.env() in match g with - | GlobRef.ConstructRef cstr -> error_wrong_numarg_constructor ?loc env cstr expanded nargs expected_nassums expected_ndecls - | GlobRef.IndRef ind -> error_wrong_numarg_inductive ?loc env ind expanded nargs expected_nassums expected_ndecls + | GlobRef.ConstructRef cstr -> error_wrong_numarg_constructor ?loc env ~cstr ~expanded ~nargs ~expected_nassums ~expected_ndecls + | GlobRef.IndRef ind -> error_wrong_numarg_inductive ?loc env ~ind ~expanded ~nargs ~expected_nassums ~expected_ndecls | _ -> assert false (** Do not raise NotEnoughArguments thanks to preconditions*) |