From 14da886bf69c13bdd5f8d700351c8253ff7f6981 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 28 May 2019 00:37:58 +0200
Subject: Fix #10264: Singleton class field data is erroneous.

---
 vernac/record.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'vernac')

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