diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-03 19:18:21 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-05 19:52:22 +0200 |
| commit | 262e3151ce483aaab3b4f60e3d1dbdf875ea05ae (patch) | |
| tree | 75d664dd62bb332cd3e8203c39e748102e0b2a57 /tactics/contradiction.ml | |
| parent | 8b8f8efe356a190ed2ae70b42688ef9170ef13b2 (diff) | |
Experimentally adding an option for automatically erasing an
hypothesis when using it in apply or rewrite (prefix ">",
undocumented), and a modifier to explicitly keep it in induction or
destruct (prefix "!", reminiscent of non-linerarity).
Also added undocumented option "Set Default Clearing Used Hypotheses"
which makes apply and rewrite default to erasing the hypothesis they
use (if ever their argument is indeed an hypothesis of the context).
Diffstat (limited to 'tactics/contradiction.ml')
| -rw-r--r-- | tactics/contradiction.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 805ecc3eb..96e8e60bb 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -94,7 +94,9 @@ let contradiction_term (c,lbind as cl) = let typ = type_of c in let _, ccl = splay_prod env sigma typ in if is_empty_type ccl then - Tacticals.New.tclTHEN (elim false cl None) (Tacticals.New.tclTRY assumption) + Tacticals.New.tclTHEN + (elim false None cl None) + (Tacticals.New.tclTRY assumption) else Proofview.tclORELSE begin |