diff options
| author | Emilio Jesus Gallego Arias | 2018-12-09 05:50:12 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-12-14 11:22:46 +0100 |
| commit | a2549c7f716e870ea19fdbfd7b5493117fe21e76 (patch) | |
| tree | e7b89cd3244d0f5c401434c0bcb6090ebecae712 /proofs/pfedit.mli | |
| parent | 7e3603069cf591c6c70ef25d4cfc72f62aa44058 (diff) | |
[proof] Rework proof interface.
- deprecate the old 5-tuple accessor in favor of a view record,
- move `name` and `kind` proof data from `Proof_global` to `Proof`,
this will prove useful in subsequent functionalizations of the
interface, in particular this is what abstract, which lives in the
monads, needs in order no to access global state.
- Note that `Proof.t` and `Proof_global.t` are redundant anyways.
Diffstat (limited to 'proofs/pfedit.mli')
| -rw-r--r-- | proofs/pfedit.mli | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 155221947a..5699320af5 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -81,8 +81,13 @@ val build_by_tactic : ?side_eff:bool -> env -> UState.t -> ?poly:polymorphic -> EConstr.types -> unit Proofview.tactic -> constr * bool * UState.t -val refine_by_tactic : env -> Evd.evar_map -> EConstr.types -> unit Proofview.tactic -> - constr * Evd.evar_map +val refine_by_tactic + : name:Id.t + -> poly:bool + -> env -> Evd.evar_map + -> EConstr.types + -> unit Proofview.tactic + -> constr * Evd.evar_map (** A variant of the above function that handles open terms as well. Caveat: all effects are purged in the returned term at the end, but other evars solved by side-effects are NOT purged, so that unexpected failures may |