diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-04 13:38:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-26 15:11:13 +0200 |
| commit | 4457e6d75affd20c1c13c0d798c490129525bcb5 (patch) | |
| tree | b5eeffe5f1a07c439fe704a6d60b2b036110df7f /API | |
| parent | a960c4db9ae93a6445f9db620f96f62b397ba8b5 (diff) | |
More precise type for universe entries.
We use an algebraic type instead of a pair of a boolean and the corresponding
data. For now, this is isomorphic, but this allows later change in the structure.
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/API/API.mli b/API/API.mli index bb24d5768..4d9904b5f 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1345,6 +1345,9 @@ sig type inline = int option type 'a proof_output = Constr.t Univ.in_universe_context_set * 'a type 'a const_entry_body = 'a proof_output Future.computation + type constant_universes_entry = + | Monomorphic_const_entry of Univ.universe_context + | Polymorphic_const_entry of Univ.universe_context type 'a definition_entry = { const_entry_body : 'a const_entry_body; (* List of section variables *) @@ -1352,8 +1355,7 @@ sig (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; const_entry_type : Constr.types option; - const_entry_polymorphic : bool; - const_entry_universes : Univ.UContext.t; + const_entry_universes : constant_universes_entry; const_entry_opaque : bool; const_entry_inline_code : bool } type parameter_entry = Context.Named.t option * bool * Constr.types Univ.in_universe_context * inline |