From 262e3151ce483aaab3b4f60e3d1dbdf875ea05ae Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 3 Aug 2014 19:18:21 +0200
Subject: 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).
---
 tactics/inv.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'tactics/inv.ml')

diff --git a/tactics/inv.ml b/tactics/inv.ml
index ee875ce27d..36affb5412 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -308,9 +308,11 @@ let projectAndApply thin id eqname names depids =
     | _ -> tac id
     end
   in
-  let deq_trailer id _ neqns =
+  let deq_trailer id clear_flag _ neqns =
     tclTHENLIST
-      [(if not (List.is_empty names) then clear [id] else tclIDTAC);
+      [apply_clear_request clear_flag
+          (not (List.is_empty names) || use_clear_hyp_by_default ())
+          (mkVar id);
        (tclMAP_i neqns (fun idopt ->
 	 tclTRY (tclTHEN
 	   (intro_move idopt MoveLast)
@@ -325,7 +327,7 @@ let projectAndApply thin id eqname names depids =
     (* and apply a trailer which again try to substitute *)
     (fun id ->
       dEqThen false (deq_trailer id)
-	(Some (ElimOnConstr (mkVar id,NoBindings))))
+	(Some (None,ElimOnConstr (mkVar id,NoBindings))))
     id
 
 let nLastDecls i tac =
-- 
cgit v1.2.3