From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- proofs/pfedit.mli | 110 +++++++++++++++++++++++++----------------------------- 1 file changed, 51 insertions(+), 59 deletions(-) (limited to 'proofs/pfedit.mli') diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index ec083e41..edbc18a3 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -1,20 +1,16 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit (** [delete_proof name] deletes proof of name [name] or fails if no proof has this name *) -val delete_proof : identifier located -> unit +val delete_proof : Id.t located -> unit (** [delete_current_proof ()] deletes current focused proof or fails if no proof is focused *) @@ -49,21 +45,6 @@ val delete_current_proof : unit -> unit val delete_all_proofs : unit -> unit -(** {6 ... } *) -(** [undo n] undoes the effect of the last [n] tactics applied to the - current proof; it fails if no proof is focused or if the ``undo'' - stack is exhausted *) - -val undo : int -> unit - -(** [undo_todepth n] resets the proof to its nth step (does [undo (d-n)] where d - is the depth of the undo stack). *) -val undo_todepth : int -> unit - -(** Returns the depth of the current focused proof stack, this is used - to put informations in coq prompt (in emacs mode). *) -val current_proof_depth: unit -> int - (** {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 @@ -75,14 +56,9 @@ val current_proof_depth: unit -> int type lemma_possible_guards = Proof_global.lemma_possible_guards val start_proof : - identifier -> goal_kind -> named_context_val -> constr -> - ?init_tac:tactic -> ?compute_guard:lemma_possible_guards -> - declaration_hook -> unit - -(** [restart_proof ()] restarts the current focused proof from the beginning - or fails if no proof is focused *) - -val restart_proof : unit -> unit + Id.t -> goal_kind -> Evd.evar_map -> named_context_val -> constr -> + ?init_tac:unit Proofview.tactic -> + Proof_global.proof_terminator -> unit (** {6 ... } *) (** [cook_proof opacity] turns the current proof (assumed completed) into @@ -90,17 +66,18 @@ val restart_proof : unit -> unit 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_proof : (Proof.proof -> unit) -> - identifier * - (Entries.definition_entry * lemma_possible_guards * goal_kind * - declaration_hook) +val cook_this_proof : + Proof_global.proof_object -> + (Id.t * + (Entries.definition_entry * Proof_global.proof_universes * goal_kind)) -(** To export completed proofs to xml *) -val set_xml_cook_proof : (goal_kind * Proof.proof -> unit) -> unit +val cook_proof : unit -> + (Id.t * + (Entries.definition_entry * Proof_global.proof_universes * goal_kind)) (** {6 ... } *) -(** [get_Proof.proof ()] returns the current focused pending proof or - raises [UserError "no focused proof"] *) +(** [get_pftreestate ()] returns the current focused pending proof. + @raise NoCurrentProof if there is no pending proof. *) val get_pftreestate : unit -> Proof.proof @@ -117,61 +94,76 @@ val get_current_goal_context : unit -> Evd.evar_map * env (** [current_proof_statement] *) val current_proof_statement : - unit -> identifier * goal_kind * types * declaration_hook + unit -> Id.t * goal_kind * types (** {6 ... } *) (** [get_current_proof_name ()] return the name of the current focused proof or failed if no proof is focused *) -val get_current_proof_name : unit -> identifier +val get_current_proof_name : unit -> Id.t (** [get_all_proof_names ()] returns the list of all pending proof names. The first name is the current proof, the other names may come in any order. *) -val get_all_proof_names : unit -> identifier list +val get_all_proof_names : unit -> Id.t list (** {6 ... } *) (** [set_end_tac tac] applies tactic [tac] to all subgoal generate - by [solve_nth] *) + by [solve] *) -val set_end_tac : tactic -> unit +val set_end_tac : Tacexpr.raw_tactic_expr -> unit (** {6 ... } *) (** [set_used_variables l] declares that section variables [l] will be used in the proof *) -val set_used_variables : identifier list -> unit -val get_used_variables : unit -> Sign.section_context option +val set_used_variables : Id.t list -> Context.section_context +val get_used_variables : unit -> Context.section_context option (** {6 ... } *) -(** [solve_nth n tac] applies tactic [tac] to the [n]th subgoal of the - current focused proof or raises a UserError if no proof is focused or - if there is no [n]th subgoal *) +(** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th + subgoal of the current focused proof or raises a [UserError] if no + proof is focused or if there is no [n]th subgoal. [solve SelectAll + tac] applies [tac] to all subgoals. *) -val solve_nth : ?with_end_tac:bool -> int -> tactic -> unit +val solve : ?with_end_tac:unit Proofview.tactic -> + Vernacexpr.goal_selector -> int option -> unit Proofview.tactic -> + Proof.proof -> Proof.proof*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 - if there is no more subgoals *) + focused proof or raises a UserError if there is no focused proof or + if there is no more subgoals. + Returns [false] if an unsafe tactic has been used. *) -val by : tactic -> unit +val by : unit Proofview.tactic -> bool (** [instantiate_nth_evar_com n c] instantiate the [n]th undefined existential variable of the current focused proof by [c] or raises a UserError if no proof is focused or if there is no such [n]th existential variable *) -val instantiate_nth_evar_com : int -> Topconstr.constr_expr -> unit +val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit -(** [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *) +(** [build_by_tactic typ tac] returns a term of type [typ] by calling + [tac]. The return boolean, if [false] indicates the use of an unsafe + tactic. *) -val build_constant_by_tactic : identifier -> named_context_val -> types -> tactic -> - Entries.definition_entry -val build_by_tactic : env -> types -> tactic -> constr +val build_constant_by_tactic : + Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind -> + types -> unit Proofview.tactic -> + Entries.definition_entry * bool * Evd.evar_universe_context + +val build_by_tactic : env -> Evd.evar_universe_context -> ?poly:polymorphic -> + types -> unit Proofview.tactic -> + constr * bool * Evd.evar_universe_context (** Declare the default tactic to fill implicit arguments *) -val declare_implicit_tactic : tactic -> unit +val declare_implicit_tactic : unit Proofview.tactic -> unit + +(** To remove the default tactic *) +val clear_implicit_tactic : unit -> unit (* Raise Exit if cannot solve *) -val solve_by_implicit_tactic : env -> Evd.evar_map -> existential -> constr +(* FIXME: interface: it may incur some new universes etc... *) +val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> constr -- cgit v1.2.3