From 30a908becf31d91592a1f7934cfa3df2d67d1834 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 22 Sep 2016 17:11:12 +0200
Subject: Revert "Merge remote-tracking branch 'github/pr/283' into trunk"

I hadn't realized that this PR uses OCaml's 4.03 inlined records
feature. I will advocate again for a switch to the latest OCaml stable
version, but meanwhile, let's revert. Sorry for the noise.

This reverts commit 3c47248abc27aa9c64120db30dcb0d7bf945bc70, reversing
changes made to ceb68d1d643ac65f500e0201f61e73cf22e6e2fb.
---
 printing/ppvernac.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 9a8ad00d08..51fc289b46 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -695,8 +695,7 @@ 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
-                     { locality = l; polymorphic = false; object_kind = dk })
+          keyword (Kindops.string_of_definition_kind (l,false,dk))
         in
         let pr_reduce = function
           | None -> mt()
-- 
cgit v1.2.3