diff options
| author | Maxime Dénès | 2016-09-20 09:11:09 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-09-20 17:18:36 +0200 |
| commit | aa29c92dfa395e2f369e81bd72cef482cdf90c65 (patch) | |
| tree | fbffe7f83d1d76a21d39bf90b93d8f948aa42143 /intf | |
| 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 'intf')
| -rw-r--r-- | intf/decl_kinds.mli | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/intf/decl_kinds.mli b/intf/decl_kinds.mli index 6a4e188337..29972f2f46 100644 --- a/intf/decl_kinds.mli +++ b/intf/decl_kinds.mli @@ -49,9 +49,13 @@ type assumption_object_kind = Definitional | Logical | Conjectural Logical | Hypothesis | Axiom *) -type assumption_kind = locality * polymorphic * assumption_object_kind +type 'a declaration_kind = { locality : locality; + polymorphic : bool; + object_kind : 'a } -type definition_kind = locality * polymorphic * definition_object_kind +type assumption_kind = assumption_object_kind declaration_kind + +type definition_kind = definition_object_kind declaration_kind (** Kinds used in proofs *) @@ -59,7 +63,7 @@ type goal_object_kind = | DefinitionBody of definition_object_kind | Proof of theorem_kind -type goal_kind = locality * polymorphic * goal_object_kind +type goal_kind = goal_object_kind declaration_kind (** Kinds used in library *) |