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.
---
 .../user-overlays/11836-ejgallego-obligations+functional.sh  | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh

(limited to 'dev/ci')

diff --git a/dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh b/dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh
new file mode 100644
index 0000000000..232ca2bf0d
--- /dev/null
+++ b/dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "11836" ] || [ "$CI_BRANCH" = "obligations+functional" ]; then
+
+    equations_CI_REF=obligations+functional
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+    paramcoq_CI_REF=obligations+functional
+    paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
+
+    mtac2_CI_REF=obligations+functional
+    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+fi
-- 
cgit v1.2.3