From 9583c0eb1771302e091880f598884b98eaec9742 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 23 Mar 2021 18:47:23 +0100
Subject: Mention label name in signature mismatch error when constant expected

Fix #13987
---
 kernel/subtyping.ml | 14 ++------------
 1 file changed, 2 insertions(+), 12 deletions(-)

(limited to 'kernel')

diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 1a4c786e43..627bf42570 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -226,6 +226,7 @@ let check_constant cst env l info1 cb2 spec2 subst1 subst2 =
     check_conv err cst poly (infer_conv_leq ?l2r:None ?evars:None ?ts:None) env t1 t2
   in
   match info1 with
+    | IndType _ | IndConstr _ -> error DefinitionFieldExpected
     | Constant cb1 ->
       let () = assert (List.is_empty cb1.const_hyps && List.is_empty cb2.const_hyps) in
       let cb1 = Declareops.subst_const_body subst1 cb1 in
@@ -254,18 +255,7 @@ let check_constant cst env l info1 cb2 spec2 subst1 subst2 =
               let c1 = Mod_subst.force_constr lc1 in
               let c2 = Mod_subst.force_constr lc2 in
               check_conv NotConvertibleBodyField cst poly (infer_conv ?l2r:None ?evars:None ?ts:None) env c1 c2))
-   | IndType ((_kn,_i),_mind1) ->
-       CErrors.user_err Pp.(str @@
-       "The kernel does not recognize yet that a parameter can be " ^
-       "instantiated by an inductive type. Hint: you can rename the " ^
-       "inductive type and give a definition to map the old name to the new " ^
-       "name.")
-   | IndConstr (((_kn,_i),_j),_mind1) ->
-      CErrors.user_err Pp.(str @@
-       "The kernel does not recognize yet that a parameter can be " ^
-       "instantiated by a constructor. Hint: you can rename the " ^
-       "constructor and give a definition to map the old name to the new " ^
-       "name.")
+
 
 let rec check_modules cst env msb1 msb2 subst1 subst2 =
   let mty1 = module_type_of_module msb1 in
-- 
cgit v1.2.3