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/kindops.ml | |
| 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/kindops.ml')
| -rw-r--r-- | library/kindops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/kindops.ml b/library/kindops.ml index 21b1bec33..3d737e5ac 100644 --- a/library/kindops.ml +++ b/library/kindops.ml @@ -24,9 +24,9 @@ let string_of_theorem_kind = function | Corollary -> "Corollary" let string_of_definition_kind def = - let (locality, poly, kind) = def in + let locality = def.locality in let error () = CErrors.anomaly (Pp.str "Internal definition kind") in - match kind with + match def.object_kind with | Definition -> begin match locality with | Discharge -> "Let" |