From dc7a4f056d97c43badaa6ca5901eafb951527d88 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 2 Dec 2020 17:22:16 +0100
Subject: Using self-documenting argument names in two exceptions of cases.ml.

Namely, WrongNumargInductive and WrongNumargConstructor.
---
 vernac/himsg.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'vernac')

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 ->
-- 
cgit v1.2.3