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.
---
 ide/texmacspp.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'ide')

diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index 637744df3e..328ddd0cdf 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -546,8 +546,7 @@ let rec tmpp v loc =
         | DefineBody (_, None  , ce, None) -> ce
         | DefineBody (_, Some _, ce, Some _) -> ce
         | DefineBody (_, None  , ce, Some _) -> ce 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_dk = Kindops.string_of_definition_kind (l, false, dk) 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