Using self-documenting argument names in two exceptions of cases.ml.

Namely, WrongNumargInductive and WrongNumargConstructor.

4 files changed, 27 insertions, 18 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*)
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
 
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 ->