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 /tactics/tactics.mllib | |
| 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 'tactics/tactics.mllib')
| -rw-r--r-- | tactics/tactics.mllib | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 6dd749aa0d..c5c7969a09 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -1,4 +1,6 @@ Declare +Proof_global +Pfedit Dnet Dn Btermdn |