diff options
| author | aspiwack | 2013-11-02 15:35:11 +0000 |
|---|---|---|
| committer | aspiwack | 2013-11-02 15:35:11 +0000 |
| commit | 80f2f9462205193885f054338ab28bfcd17de965 (patch) | |
| tree | b6c9e46cbc54080ec260282558abe9e8fc609723 /plugins/funind/functional_principles_proofs.ml | |
| 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 'plugins/funind/functional_principles_proofs.ml')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 2da4b61478..8c2fdb7eb5 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -983,7 +983,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) lemma_type (fun _ _ -> ()); - Pfedit.by (Proofview.V82.tactic prove_replacement); + ignore (Pfedit.by (Proofview.V82.tactic prove_replacement)); Lemmas.save_named false |