diff options
| author | Gaëtan Gilbert | 2019-01-30 14:39:28 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-17 15:44:30 +0100 |
| commit | a9f0fd89cf3bb4b728eb451572a96f8599211380 (patch) | |
| tree | 577b7330af67793041cfaba8414005f93fc49c88 /vernac/classes.ml | |
| parent | a49077ef67b8e70696ecacc311fc3070d1b7b461 (diff) | |
Separate variance and universe fields in inductives.
I think the usage looks cleaner this way.
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index ea434dbc4f..27d8b7390d 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -374,7 +374,7 @@ let context poly l = let univs = match ctx with | [] -> assert false - | [_] -> Evd.const_univ_entry ~poly sigma + | [_] -> Evd.univ_entry ~poly sigma | _::_::_ -> if Lib.sections_are_opened () then @@ -384,19 +384,19 @@ let context poly l = begin let uctx = Evd.universe_context_set sigma in Declare.declare_universe_context poly uctx; - if poly then Polymorphic_const_entry ([||], Univ.UContext.empty) - else Monomorphic_const_entry Univ.ContextSet.empty + if poly then Polymorphic_entry ([||], Univ.UContext.empty) + else Monomorphic_entry Univ.ContextSet.empty end else if poly then (* Multiple polymorphic axioms: they are all polymorphic the same way. *) - Evd.const_univ_entry ~poly sigma + Evd.univ_entry ~poly sigma else (* Multiple monomorphic axioms: declare universes separately to avoid redeclaring them. *) begin let uctx = Evd.universe_context_set sigma in Declare.declare_universe_context poly uctx; - Monomorphic_const_entry Univ.ContextSet.empty + Monomorphic_entry Univ.ContextSet.empty end in let fn status (id, b, t) = |