From c951e2ed88437c613bd4355b32547f9c39269eed Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 20 Aug 2019 00:02:28 +0200
Subject: [declare] Move proof_entry type to declare, put interactive proof
 data on top of declare.

This PR is a follow up to #10406 , moving the then introduced
`proof_entry` type to `Declare`.

This makes sense as `Declare` is the main consumer of the entry type,
and already provides the constructors for it.

This is a step towards making the entry type private, which will allow
us to enforce / handle invariants on entry data better.

A side-effect of this PR is that now `Proof_global` does depend on
`Declare`, not the other way around, but that makes sense given that
closing an interactive proof will be a client of declare.

Indeed, all `Declare` / `Pfedit` / and `Proof_global` are tied into
tactics due to `abstract`, at some point we may be able to unify all
them into a single file in `vernac`.
---
 vernac/declareDef.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/declareDef.ml')

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 5e4f2dcd34..1926faaf0e 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -44,7 +44,7 @@ end
 
 (* Locality stuff *)
 let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
-  let fix_exn = Future.fix_exn_of ce.Proof_global.proof_entry_body in
+  let fix_exn = Future.fix_exn_of ce.proof_entry_body in
   let gr = match scope with
   | Discharge ->
       let () =
-- 
cgit v1.2.3