diff options
| author | Emilio Jesus Gallego Arias | 2019-08-20 00:02:28 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-08-27 16:57:46 +0200 |
| commit | c951e2ed88437c613bd4355b32547f9c39269eed (patch) | |
| tree | c4ff648c17b89796e726446718181104b1f7f768 /dev/ci | |
| parent | 1e1d5bf3879424688fa9231ba057b05d86674d22 (diff) | |
[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`.
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh | 6 |
1 files changed, 6 insertions, 0 deletions
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 |