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/ind_tables.ml | |
| 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/ind_tables.ml')
| -rw-r--r-- | tactics/ind_tables.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index e2ef05461b..1f973ace6f 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -125,7 +125,7 @@ let define internal role id c poly univs = let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in let univs = UState.univ_entry ~poly ctx in let entry = { - Proof_global.proof_entry_body = + Declare.proof_entry_body = Future.from_val ((c,Univ.ContextSet.empty), Evd.empty_side_effects); proof_entry_secctx = None; |