Fix #10264: Singleton class field data is erroneous.

1 files changed, 4 insertions, 2 deletions

diff --git a/vernac/record.ml b/vernac/record.ml
index f737a8c524..d617b13db4 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -588,12 +588,14 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
 let add_constant_class env sigma cst =
   let ty, univs = Typeops.type_of_global_in_context env (ConstRef cst) in
   let r = (Environ.lookup_constant cst env).const_relevance in
-  let ctx, arity = decompose_prod_assum ty in
+  let ctx, _ = decompose_prod_assum ty in
+  let args = Context.Rel.to_extended_vect Constr.mkRel 0 ctx in
+  let t = mkApp (mkConstU (cst, Univ.make_abstract_instance univs), args) in
   let tc = 
     { cl_univs = univs;
       cl_impl = ConstRef cst;
       cl_context = (List.map (const None) ctx, ctx);
-      cl_props = [LocalAssum (make_annot Anonymous r, arity)];
+      cl_props = [LocalAssum (make_annot Anonymous r, t)];
       cl_projs = [];
       cl_strict = !typeclasses_strict;
       cl_unique = !typeclasses_unique