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".
---
 printing/ppvernac.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 51fc289b46..9a8ad00d08 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -695,7 +695,8 @@ module Make
       | VernacDefinition (d,id,b) -> (* A verifier... *)
         let pr_def_token (l,dk) =
           let l = match l with Some x -> x | None -> Decl_kinds.Global in
-          keyword (Kindops.string_of_definition_kind (l,false,dk))
+          keyword (Kindops.string_of_definition_kind
+                     { locality = l; polymorphic = false; object_kind = dk })
         in
         let pr_reduce = function
           | None -> mt()
-- 
cgit v1.2.3