[coqchk] Fix checking of records in module signatures

1 files changed, 5 insertions, 3 deletions

diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 0916d98ddf..e2c605dde8 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -198,9 +198,11 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
     assert (Array.length mib2.mind_packets = 1);
     assert (Array.length mib1.mind_packets.(0).mind_user_lc = 1);
     assert (Array.length mib2.mind_packets.(0).mind_user_lc = 1);
-    check
-      (fun l1 l2 -> List.equal Name.equal l1 l2)
-      (fun mib -> names_prod_letin mib.mind_packets.(0).mind_user_lc.(0));
+    check (List.equal Name.equal)
+      (fun mib ->
+         let nparamdecls = List.length mib.mind_params_ctxt in
+         let names = names_prod_letin (mib.mind_packets.(0).mind_user_lc.(0)) in
+         snd (List.chop nparamdecls names))
   end;
   (* we first check simple things *)
   Array.iter2 check_packet mib1.mind_packets mib2.mind_packets;