From 230f135eb7ba80b4be74da493f205a7eb1b5fa3d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 28 Aug 2018 13:40:45 +0200
Subject: Do not redeclare universes for monomorphic operational typeclasses

eg in [Class Foo (A:Type) := foo : A.] the universe should be
declared when declaring the constant [Foo] and not [foo].
---
 vernac/record.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/vernac/record.ml b/vernac/record.ml
index 6b5c538df2..8dd123de15 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -476,10 +476,11 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
       let cst = Declare.declare_constant id
 	(DefinitionEntry class_entry, IsDefinition Definition)
       in
-      let cstu = (cst, match univs with
-        | Polymorphic_const_entry univs -> Univ.UContext.instance univs
-        | Monomorphic_const_entry _ -> Univ.Instance.empty)
+      let inst, univs = match univs with
+        | Polymorphic_const_entry uctx -> Univ.UContext.instance uctx, univs
+        | Monomorphic_const_entry _ -> Univ.Instance.empty, Monomorphic_const_entry Univ.ContextSet.empty
       in
+      let cstu = (cst, inst) in
       let inst_type = appvectc (mkConstU cstu)
 			       (Termops.rel_vect 0 (List.length params)) in
       let proj_type =
-- 
cgit v1.2.3