From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- proofs/pfedit.mli | 140 ++++++++++++++++++++++++------------------------------ 1 file changed, 63 insertions(+), 77 deletions(-) (limited to 'proofs/pfedit.mli') diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 05c329c1..7297b975 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -1,14 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* bool -(* [check_no_pending_proofs ()] fails if there is still some proof in +(** [check_no_pending_proofs ()] fails if there is still some proof in progress *) val check_no_pending_proofs : unit -> unit -(*s [delete_proof name] deletes proof of name [name] or fails if no proof +(** {6 ... } *) +(** [delete_proof name] deletes proof of name [name] or fails if no proof has this name *) val delete_proof : identifier located -> unit -(* [delete_current_proof ()] deletes current focused proof or fails if +(** [delete_current_proof ()] deletes current focused proof or fails if no proof is focused *) val delete_current_proof : unit -> unit -(* [delete_all_proofs ()] deletes all open proofs if any *) +(** [delete_all_proofs ()] deletes all open proofs if any *) val delete_all_proofs : unit -> unit -(*s [undo n] undoes the effect of the last [n] tactics applied to the +(** {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 -(* Same as undo, but undoes the current proof stack to reach depth - [n]. This is used in [vernac_backtrack]. *) -val undo_todepth : 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 +(** 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 -(* [set_undo (Some n)] sets the size of the ``undo'' stack; [set_undo None] - sets the size to the default value (12) *) - -val set_undo : int option -> unit -val get_undo : unit -> int option - -(*s [start_proof s str env t hook tac] starts a proof of name [s] and +(** {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) *) -type lemma_possible_guards = int list list +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 +(** [restart_proof ()] restarts the current focused proof from the beginning or fails if no proof is focused *) val restart_proof : unit -> unit -(*s [resume_last_proof ()] focus on the last unfocused proof or fails +(** {6 ... } *) +(** [resume_last_proof ()] focus on the last unfocused proof or fails if there is no suspended proofs *) val resume_last_proof : unit -> unit -(* [resume_proof name] focuses on the proof of name [name] or - raises [UserError] if no proof has name [name] *) +(** [resume_proof name] focuses on the proof of name [name] or + raises [NoSuchProof] if no proof has name [name]. + + It doesn't [suspend_proof ()] before. *) val resume_proof : identifier located -> unit -(* [suspend_proof ()] unfocuses the current focused proof or +(** [suspend_proof ()] unfocuses the current focused proof or failed with [UserError] if no proof is currently focused *) val suspend_proof : unit -> unit -(*s [cook_proof opacity] turns the current proof (assumed completed) into +(** {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_proof : (Refiner.pftreestate -> unit) -> +val cook_proof : (Proof.proof -> unit) -> identifier * - (Entries.definition_entry * lemma_possible_guards * goal_kind * - declaration_hook) + (Entries.definition_entry * lemma_possible_guards * goal_kind * + declaration_hook) -(* To export completed proofs to xml *) -val set_xml_cook_proof : (goal_kind * pftreestate -> unit) -> unit +(** To export completed proofs to xml *) +val set_xml_cook_proof : (goal_kind * Proof.proof -> unit) -> unit -(*s [get_pftreestate ()] returns the current focused pending proof or +(** {6 ... } *) +(** [get_Proof.proof ()] returns the current focused pending proof or raises [UserError "no focused proof"] *) -val get_pftreestate : unit -> pftreestate +val get_pftreestate : unit -> Proof.proof -(* [get_end_tac ()] returns the current tactic to apply to all new subgoal *) - -val get_end_tac : unit -> tactic option - -(* [get_goal_context n] returns the context of the [n]th subgoal of +(** [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 *) val get_goal_context : int -> Evd.evar_map * env -(* [get_current_goal_context ()] works as [get_goal_context 1] *) +(** [get_current_goal_context ()] works as [get_goal_context 1] *) val get_current_goal_context : unit -> Evd.evar_map * env -(* [current_proof_statement] *) +(** [current_proof_statement] *) val current_proof_statement : unit -> identifier * goal_kind * types * declaration_hook -(*s [get_current_proof_name ()] return the name of the current focused +(** {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 -(* [get_all_proof_names ()] returns the list of all pending proof names *) +(** [get_all_proof_names ()] returns the list of all pending proof names *) val get_all_proof_names : unit -> identifier list -(*s [set_end_tac tac] applies tactic [tac] to all subgoal generate +(** {6 ... } *) +(** [set_end_tac tac] applies tactic [tac] to all subgoal generate by [solve_nth] *) val set_end_tac : tactic -> unit -(*s [solve_nth n tac] applies tactic [tac] to the [n]th subgoal of the +(** {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 + +(** {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 *) -val solve_nth : int -> tactic -> unit +val solve_nth : ?with_end_tac:bool -> int -> tactic -> unit -(* [by tac] applies tactic [tac] to the 1st subgoal of the current +(** [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 *) val by : tactic -> unit -(* [instantiate_nth_evar_com n c] instantiate the [n]th undefined +(** [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 -(*s To deal with subgoal focus *) - -val make_focus : int -> unit -val focus : unit -> int -val focused_goal : unit -> int -val subtree_solved : unit -> bool -val tree_solved : unit -> bool -val top_tree_solved : unit -> bool +(** [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *) -val reset_top_of_tree : unit -> unit -val reset_top_of_script : unit -> unit - -val traverse : int -> unit -val traverse_nth_goal : int -> unit -val traverse_next_unproven : unit -> unit -val traverse_prev_unproven : unit -> unit - - -(* These two functions make it possible to implement more elaborate - proof and goal management, as it is done, for instance in pcoq *) - -val traverse_to : int list -> unit -val mutate : (pftreestate -> pftreestate) -> unit +val build_constant_by_tactic : identifier -> named_context_val -> types -> tactic -> + Entries.definition_entry +val build_by_tactic : env -> types -> tactic -> constr +(** Declare the default tactic to fill implicit arguments *) -(* [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *) +val declare_implicit_tactic : tactic -> unit -val build_constant_by_tactic : identifier -> named_context_val -> types -> tactic -> - Entries.definition_entry -val build_by_tactic : types -> tactic -> constr +(* Raise Exit if cannot solve *) +val solve_by_implicit_tactic : env -> Evd.evar_map -> existential -> constr -- cgit v1.2.3