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/comDefinition.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'vernac/comDefinition.ml')

diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 853f2c9aa3..b3cc0a4236 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -10,7 +10,6 @@
 
 open Pp
 open Util
-open Entries
 open Redexpr
 open Constrintern
 open Pretyping
@@ -86,12 +85,12 @@ let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt =
   in
   if program_mode then
     let env = Global.env () in
-    let (c,ctx), sideff = Future.force ce.const_entry_body in
+    let (c,ctx), sideff = Future.force ce.Proof_global.proof_entry_body in
     assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private);
     assert(Univ.ContextSet.is_empty ctx);
     Obligations.check_evars env evd;
     let c = EConstr.of_constr c in
-    let typ = match ce.const_entry_type with
+    let typ = match ce.Proof_global.proof_entry_type with
       | Some t -> EConstr.of_constr t
       | None -> Retyping.get_type_of env evd c
     in
-- 
cgit v1.2.3