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`.
---
 dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh

(limited to 'dev')

diff --git a/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh b/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh
new file mode 100644
index 0000000000..6dc44aa627
--- /dev/null
+++ b/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10674" ] || [ "$CI_BRANCH" = "proofs+declare_unif" ]; then
+
+    equations_CI_REF=proofs+declare_unif
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi
-- 
cgit v1.2.3