From 5ae026cebc6c468373459af950533bee0c02501a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 11 May 2020 04:09:31 +0200
Subject: [declare] Grand unification of the proof save path.

We complete some arduous refactoring in order to bring all the
internals and code of constant / proof saving into the same module.

In particular, this PR moves the remaining parts of proof saving from
`Lemmas` to `Declare`.

The reduction in exposed internals is considerable; in particular, we
remove the export of the internals of `proof_entry` and `proof_object`
[used in delayed proofs], which will allow us to start to address many
issues with the current setup, such as #10363 .

There are still some TODOs, that will be addressed in subsequent PRs:

- Remove `declare_constant` in favor of higher-level APIs
- Then, remove access to `proof_entry` entirely
- Refactor current very verbose handling of proof info.
- Remove compat modules / API.
- Rework handling of delayed proofs [this may be hard due to state and the STM]
- Reify Hook API for the case where it acts as a continuation [that is to say, declaring constants from the Hook]

List of remaining offenders for `proof_entry` / `declare_constant` in
the codebase:

- File "vernac/comHints.ml"
- File "vernac/indschemes.ml"
- File "vernac/comProgramFixpoint.ml"
- File "vernac/comAssumption.ml"
- File "vernac/record.ml"
- File "plugins/ltac/leminv.ml"
- File "plugins/setoid_ring/newring.ml"
- File "plugins/funind/recdef.ml"
- File "plugins/funind/gen_principle.ml"
---
 stm/stm.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 177a76e64b..04f08e488b 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1684,7 +1684,9 @@ end = struct (* {{{ *)
       (* STATE We use the state resulting from reaching start. *)
       let st = Vernacstate.freeze_interp_state ~marshallable:false in
       ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~info ~loc ~control:[] (Proved (opaque,None)));
-      `OK proof
+      (* Is this name the same than the one in scope? *)
+      let name = Declare.get_po_name proof in
+      `OK name
       end
     with e ->
       let (e, info) = Exninfo.capture e in
@@ -1723,7 +1725,7 @@ end = struct (* {{{ *)
     | `ERROR -> exit 1
     | `ERROR_ADMITTED -> cst, false
     | `OK_ADMITTED -> cst, false
-    | `OK { Declare.name } ->
+    | `OK name ->
         let con = Nametab.locate_constant (Libnames.qualid_of_ident name) in
         let c = Global.lookup_constant con in
         let o = match c.Declarations.const_body with
-- 
cgit v1.2.3