diff options
| author | Hugo Herbelin | 2014-08-03 19:18:21 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-08-05 19:52:22 +0200 |
| commit | 262e3151ce483aaab3b4f60e3d1dbdf875ea05ae (patch) | |
| tree | 75d664dd62bb332cd3e8203c39e748102e0b2a57 /toplevel/auto_ind_decl.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 'toplevel/auto_ind_decl.ml')
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 12 |
1 files changed, 6 insertions, 6 deletions
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 ( |