diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-09-20 09:11:09 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-09-20 17:18:36 +0200 |
| commit | aa29c92dfa395e2f369e81bd72cef482cdf90c65 (patch) | |
| tree | fbffe7f83d1d76a21d39bf90b93d8f948aa42143 /library/lib.mli | |
| parent | 424de98770e1fd8c307a7cd0053c268a48532463 (diff) | |
Stylistic improvements in intf/decl_kinds.mli.
We get rid of tuples containing booleans (typically for universe
polymorphism) by replacing them with records.
The previously common idom:
if pi2 kind (* polymorphic *) then ... else ...
becomes:
if kind.polymorphic then ... else ...
To make the construction and destruction of these records lightweight,
the labels of boolean arguments for universe polymorphism are now
usually also called "polymorphic".
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/library/lib.mli b/library/lib.mli index 092643c2d..e905ee57e 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -176,11 +176,11 @@ val variable_section_segment_of_reference : Globnames.global_reference -> variab val section_instance : Globnames.global_reference -> Univ.universe_instance * Names.Id.t array val is_in_section : Globnames.global_reference -> bool -val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit +val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> polymorphic:bool -> Univ.universe_context_set -> unit val add_section_context : Univ.universe_context_set -> unit -val add_section_constant : Decl_kinds.polymorphic -> +val add_section_constant : polymorphic:bool -> Names.constant -> Context.Named.t -> unit -val add_section_kn : Decl_kinds.polymorphic -> +val add_section_kn : polymorphic:bool -> Names.mutual_inductive -> Context.Named.t -> unit val replacement_context : unit -> Opaqueproof.work_list |