diff options
Diffstat (limited to 'proofs/pfedit.mli')
| -rw-r--r-- | proofs/pfedit.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index d676a0874..5a317a956 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -35,11 +35,11 @@ val start_proof : val cook_this_proof : Proof_global.proof_object -> (Id.t * - (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind)) + (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind)) val cook_proof : unit -> (Id.t * - (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind)) + (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind)) (** {6 ... } *) (** [get_goal_context n] returns the context of the [n]th subgoal of @@ -74,7 +74,7 @@ val current_proof_statement : val solve : ?with_end_tac:unit Proofview.tactic -> Vernacexpr.goal_selector -> int option -> unit Proofview.tactic -> - Proof.proof -> Proof.proof*bool + Proof.t -> Proof.t * bool (** [by tac] applies tactic [tac] to the 1st subgoal of the current focused proof or raises a UserError if there is no focused proof or |