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).

1 files changed, 1 insertions, 2 deletions

diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 9b4c62f87e..1e8fad98ec 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -169,5 +169,4 @@ Section Acc_generator.
     end.
 
 
-End Acc_generator. 
- 
\ No newline at end of file
+End Acc_generator.