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".
---
 intf/decl_kinds.mli | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'intf')

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 *)
 
-- 
cgit v1.2.3