From aa29c92dfa395e2f369e81bd72cef482cdf90c65 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 20 Sep 2016 09:11:09 +0200
Subject: 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".
---
 ide/texmacspp.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'ide')

diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index 328ddd0cdf..637744df3e 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) ->
-- 
cgit v1.2.3