diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:35:11 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:35:11 +0000 |
| commit | 80f2f9462205193885f054338ab28bfcd17de965 (patch) | |
| tree | b6c9e46cbc54080ec260282558abe9e8fc609723 /proofs/pfedit.mli | |
| parent | d45d2232e9dae87162a841a21cc708769259a184 (diff) | |
The tactic [admit] exits with the "unsafe" status.
It is highlighted in yellow in Coqide.
The unsafe status is tracked throughout the execution of tactics such that
nested calls to admit are caught.
Many function (mainly those building constr with tactics such as typeclass
related stuff, and Function, and a few other like eauto's use of Hint Extern)
drop the unsafe status. This is unfortunate, but a lot of refactoring would
be in order.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16977 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/pfedit.mli')
| -rw-r--r-- | proofs/pfedit.mli | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 3a0c25c46..73f12db98 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -136,13 +136,14 @@ val get_used_variables : unit -> Context.section_context option if there is no [n]th subgoal *) val solve_nth : ?with_end_tac:unit Proofview.tactic -> int -> unit Proofview.tactic -> - Proof.proof -> Proof.proof + 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 *) + if there is no more subgoals. + Returns [false] if an unsafe tactic has been used. *) -val by : unit Proofview.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 @@ -151,12 +152,14 @@ val by : unit Proofview.tactic -> 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 : Id.t -> named_context_val -> ?goal_kind:goal_kind -> - types -> unit Proofview.tactic -> Entries.definition_entry -val build_by_tactic : env -> types -> unit Proofview.tactic -> constr + types -> unit Proofview.tactic -> Entries.definition_entry * bool +val build_by_tactic : env -> types -> unit Proofview.tactic -> constr * bool (** Declare the default tactic to fill implicit arguments *) |