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).
---
 toplevel/auto_ind_decl.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 0fbf0654f7..15b370b06e 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -79,12 +79,12 @@ let andb = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb
 
 let induct_on c =
   induction false
-    [Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
+    [None,Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
     None (None,None) None
 
 let destruct_on_using c id =
   destruct false
-    [Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
+    [None,Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
     None
     (None,Some (dl,IntroOrAndPattern [
                                     [dl,IntroAnonymous];
@@ -93,7 +93,7 @@ let destruct_on_using c id =
 
 let destruct_on c =
   destruct false
-    [Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
+    [None,Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
     None (None,None) None
 
 (* reconstruct the inductive with the correct deBruijn indexes *)
@@ -589,10 +589,10 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
 *)
                     Tacticals.New.tclREPEAT (
                       Tacticals.New.tclTHENLIST [
-                         apply_in false false freshz [Loc.ghost, (andb_prop(), NoBindings)] None;
+                         Simple.apply_in freshz (andb_prop());
                          Proofview.Goal.enter begin fun gl ->
                            let fresht = fresh_id (Id.of_string "Z") gl in
-                            (destruct false [Tacexpr.ElimOnConstr
+                            (destruct false [None,Tacexpr.ElimOnConstr
                                       (Evd.empty,((mkVar freshz,NoBindings)))]
                                   None
                                   (None, Some (dl,IntroOrAndPattern [[
@@ -723,7 +723,7 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec =
                      Tacticals.New.tclTRY (
                       Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None)
                      );
-                     Equality.inj None false (mkVar freshz,NoBindings);
+                     Equality.inj None false None (mkVar freshz,NoBindings);
 		     intros; (Proofview.V82.tactic simpl_in_concl);
                      Auto.default_auto;
                      Tacticals.New.tclREPEAT (
-- 
cgit v1.2.3