diff options
| author | Matthieu Sozeau | 2018-09-19 10:29:01 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2018-09-19 10:29:01 +0200 |
| commit | 6d74efabf11768ca1df3a2f3d5a65d25f7f95b01 (patch) | |
| tree | 8c5648169e305e9b4038b6f04efb5a155e2f2115 /vernac | |
| parent | eeab61130a2867cd7f40f86a25911b27d1962d3a (diff) | |
| parent | fa4c0aab3eace78fe283f4630e4db5ed076d267e (diff) | |
Merge PR #8341: Reduce universe redeclarations (catching AlreadyDeclared)
Diffstat (limited to 'vernac')
| -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 d36586d062..7ab2b50764 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -487,10 +487,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 = |