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 /vernac/comDefinition.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 'vernac/comDefinition.ml')
| -rw-r--r-- | vernac/comDefinition.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 57de719cb4..9745358ba2 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -85,12 +85,12 @@ let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_o in if program_mode then let env = Global.env () in - let (c,ctx), sideff = Future.force ce.Proof_global.proof_entry_body in + let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private); assert(Univ.ContextSet.is_empty ctx); Obligations.check_evars env evd; let c = EConstr.of_constr c in - let typ = match ce.Proof_global.proof_entry_type with + let typ = match ce.Declare.proof_entry_type with | Some t -> EConstr.of_constr t | None -> Retyping.get_type_of env evd c in |