aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init/Wf.v
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-08-03 19:18:21 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-08-05 19:52:22 +0200
commit262e3151ce483aaab3b4f60e3d1dbdf875ea05ae (patch)
tree75d664dd62bb332cd3e8203c39e748102e0b2a57 /theories/Init/Wf.v
parent8b8f8efe356a190ed2ae70b42688ef9170ef13b2 (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 'theories/Init/Wf.v')
-rw-r--r--theories/Init/Wf.v3
1 files changed, 1 insertions, 2 deletions
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 9b4c62f87..1e8fad98e 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.