From 809291d5ef7371bfe8841b95126c0332da55578f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 15 Mar 2020 17:52:16 -0400
Subject: [obligations] Pre-functionalize Program state

In our quest to unify all the declaration paths, an important step
is to account for the state pertaining to `Program` declarations.

Whereas regular proofs keep are kept in a stack-like structure;
obligations for constants defined by `Program` are stored in a global
map which is manipulated by almost regular open/close proof primitives.

This PR is in preparation for the switch to a purely functional state
in #11836 ; the full switch requires deeper changes so it is helpful
to have this PR preparing most of the structure.

Most of the PR is routine; only remarkable change is that the hook for
admitted obligations is now called explicitly in `finish_admitted` as
it had to learn about the different types of proof_endings. Before,
obligations set it in `start_lemma` but only used in the `Admitted`
path.
---
 stm/stm.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index b296f8f08f..aa5a14c7dd 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -202,7 +202,7 @@ let mkTransCmd cast cids ceff cqueue =
 (* Parts of the system state that are morally part of the proof state *)
 let summary_pstate = Evarutil.meta_counter_summary_tag,
                      Evd.evar_counter_summary_tag,
-                     DeclareObl.program_tcc_summary_tag
+                     DeclareObl.State.prg_tag
 
 type cached_state =
   | EmptyState
@@ -878,7 +878,7 @@ end = struct (* {{{ *)
     Vernacstate.LemmaStack.t option *
     int *                                   (* Evarutil.meta_counter_summary_tag *)
     int *                                   (* Evd.evar_counter_summary_tag *)
-    DeclareObl.ProgramDecl.t CEphemeron.key Names.Id.Map.t (* Obligations.program_tcc_summary_tag *)
+    DeclareObl.State.t
 
   type partial_state =
     [ `Full of Vernacstate.t
-- 
cgit v1.2.3