diff options
| author | Gaëtan Gilbert | 2018-08-28 13:40:45 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-09-13 15:05:57 +0200 |
| commit | 230f135eb7ba80b4be74da493f205a7eb1b5fa3d (patch) | |
| tree | 633647a5a5a8b32ea0bd67d817071715dfc7f908 | |
| parent | d3fee162c5e2f39b313cde1e1fa738480d960163 (diff) | |
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].
| -rw-r--r-- | vernac/record.ml | 7 |
1 files 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 = |