From 54788df72ce79998ee27db362401a56bda4daceb Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 15 Mar 2020 17:52:16 -0400
Subject: [obligations] 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.

We make this manipulation explicit by handling the program state
functionally, in a similar way than we already do for lemmas.

This requires to extend the proof DSL a bit; but IMO changes are
acceptable given the gain.

Most of the PR is routine; only remarkable change is that the hook is
called explicitly in `finish_admitted` as it had to learn about the
different types of proof_endings.

Note that we could have gone deeper and use the type system to refine
the core proof type; IMO it is still too preliminary so it is better
to do this step as an intermediate one towards a deeper unification.
---
 coqpp/coqpp_main.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'coqpp')

diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 39ca5413cc..ffde49f2ac 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -339,6 +339,9 @@ let understand_state = function
   | "proof" -> "VtModifyProof", false
   | "proof_opt_query" -> "VtReadProofOpt", false
   | "proof_query" -> "VtReadProof", false
+  | "read_program" -> "VtReadProgram", false
+  | "program" -> "VtModifyProgram", false
+  | "declare_program" -> "VtDeclareProgram", false
   | s -> fatal ("unsupported state specifier: " ^ s)
 
 let print_body_state state fmt r =
-- 
cgit v1.2.3


From a164eaafad33ccbc2b0bdbb75147a54ebe3a9848 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 29 Jun 2020 15:00:28 +0200
Subject: [obligations] Allow to simultaneously open a proof and add
 obligations

---
 coqpp/coqpp_main.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'coqpp')

diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index ffde49f2ac..2735c5b5eb 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -342,6 +342,7 @@ let understand_state = function
   | "read_program" -> "VtReadProgram", false
   | "program" -> "VtModifyProgram", false
   | "declare_program" -> "VtDeclareProgram", false
+  | "program_interactive" -> "VtOpenProofProgram", false
   | s -> fatal ("unsupported state specifier: " ^ s)
 
 let print_body_state state fmt r =
-- 
cgit v1.2.3