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.
---
 plugins/funind/functional_principles_proofs.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'plugins/funind/functional_principles_proofs.ml')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index bba7b3c599..527f4f0b12 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -996,9 +996,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
       Ensures by: obvious
       i*)
     (mk_equation_id f_id)
-    Decl_kinds.{ locality = Global;
-                 polymorphic = Flags.is_universe_polymorphism ();
-                 object_kind = Proof Theorem }
+    (Decl_kinds.Global, Flags.is_universe_polymorphism (), (Decl_kinds.Proof Decl_kinds.Theorem))
     evd
   lemma_type
   (Lemmas.mk_hook (fun _ _ -> ()));
-- 
cgit v1.2.3