diff options
Diffstat (limited to 'proofs/pfedit.mli')
| -rw-r--r-- | proofs/pfedit.mli | 28 |
1 files changed, 0 insertions, 28 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 50ce267c81..155221947a 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -16,34 +16,6 @@ open Environ open Decl_kinds (** {6 ... } *) -(** [start_proof s str env t hook tac] starts a proof of name [s] and - conclusion [t]; [hook] is optionally a function to be applied at - proof end (e.g. to declare the built constructions as a coercion - or a setoid morphism); init_tac is possibly a tactic to - systematically apply at initialization time (e.g. to start the - proof of mutually dependent theorems) *) - -val start_proof : - Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr -> - ?init_tac:unit Proofview.tactic -> - Proof_global.proof_terminator -> unit - -(** {6 ... } *) -(** [cook_proof opacity] turns the current proof (assumed completed) into - a constant with its name, kind and possible hook (see [start_proof]); - it fails if there is no current proof of if it is not completed; - it also tells if the guardness condition has to be inferred. *) - -val cook_this_proof : - Proof_global.proof_object -> - (Id.t * - (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind)) - -val cook_proof : unit -> - (Id.t * - (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 the current focused proof or raises a [UserError] if there is no focused proof or if there is no more subgoals *) |