From f597952e1b216ca5adf9f782c736f4cfe705ef02 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 16 Jun 2019 19:09:25 +0200
Subject: Duplicate the type of constant entries in Proof_global.

This allows to desynchronize the kernel-facing API from the proof-facing one.
---
 vernac/declareDef.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'vernac/declareDef.ml')

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 42327d6bdd..a467c22ede 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -10,7 +10,6 @@
 
 open Decl_kinds
 open Declare
-open Entries
 open Globnames
 open Impargs
 
@@ -38,7 +37,7 @@ end
 
 (* Locality stuff *)
 let declare_definition ident (local, p, k) ?hook_data ce pl imps =
-  let fix_exn = Future.fix_exn_of ce.const_entry_body in
+  let fix_exn = Future.fix_exn_of ce.Proof_global.proof_entry_body in
   let gr = match local with
   | Discharge ->
       let _ = declare_variable ident (Lib.cwd(), SectionLocalDef ce, IsDefinition k) in
-- 
cgit v1.2.3