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 /ide | |
| 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 'ide')
| -rw-r--r-- | ide/texmacspp.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index 328ddd0cd..637744df3 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -546,7 +546,8 @@ let rec tmpp v loc = | DefineBody (_, None , ce, None) -> ce | DefineBody (_, Some _, ce, Some _) -> ce | DefineBody (_, None , ce, Some _) -> ce in - let str_dk = Kindops.string_of_definition_kind (l, false, dk) in + let def_kind = { locality = l; polymorphic = false; object_kind = dk } in + let str_dk = Kindops.string_of_definition_kind def_kind in let str_id = Id.to_string id in (xmlDef str_dk str_id loc [pp_expr e]) | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement, None) ], b) -> |