From 5c5b5906426f38323fc5d63f4dc634672ebd2649 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 8 Dec 2015 23:34:38 +0100 Subject: Adding an unshelve tactical. This tactical is inspired by discussions on the Coq-club list. For now it is still undocumented, and there is room left for design issues. --- tactics/extratactics.ml4 | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'tactics') diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 9ffcd2dcff..1355499e48 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -21,6 +21,7 @@ open Util open Evd open Equality open Misctypes +open Proofview.Notations DECLARE PLUGIN "extratactics" @@ -864,6 +865,15 @@ TACTIC EXTEND shelve_unifiable [ Proofview.shelve_unifiable ] END +(* Unshelves the goal shelved by the tactic. *) +TACTIC EXTEND unshelve +| [ "unshelve" tactic(t) ] -> + [ + Proofview.with_shelf (Tacinterp.eval_tactic t) >>= fun (gls, ()) -> + Proofview.Unsafe.tclNEWGOALS gls + ] +END + (* Command to add every unshelved variables to the focus *) VERNAC COMMAND EXTEND Unshelve [ "Unshelve" ] -- cgit v1.2.3 From 8ea758fbb392e270e6a8d2287dbb5b0455d99368 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 9 Dec 2015 11:56:52 +0100 Subject: Fixing parsing of the unshelve tactical. Now [unshelve tac1; tac2] is parsed as [(unshelve tac1); tac2]. --- tactics/extratactics.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 1355499e48..827d2e25a6 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -867,7 +867,7 @@ END (* Unshelves the goal shelved by the tactic. *) TACTIC EXTEND unshelve -| [ "unshelve" tactic(t) ] -> +| [ "unshelve" tactic0(t) ] -> [ Proofview.with_shelf (Tacinterp.eval_tactic t) >>= fun (gls, ()) -> Proofview.Unsafe.tclNEWGOALS gls -- cgit v1.2.3 From a6f1944809e4caa6c99deb8c508dab9ad0e0071e Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 10 Dec 2015 16:02:15 +0100 Subject: Silently ignore requests to _not_ clear something when that something cannot be cleared. This should fix the contrib failures on tactics like "destruct (0)". --- tactics/tactics.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ce8b9b3dbd..536a10eaa7 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -277,7 +277,8 @@ let apply_clear_request clear_flag dft c = error "keep/clear modifiers apply only to hypothesis names." in let clear = match clear_flag with | None -> dft && isVar c - | Some clear -> check_isvar c; clear in + | Some true -> check_isvar c; true + | Some false -> false in if clear then Proofview.V82.tactic (thin [destVar c]) else Tacticals.New.tclIDTAC -- cgit v1.2.3 From cdaf8e2ed109bd117da2366a279fa575d7b6185a Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 10 Dec 2015 19:14:19 +0100 Subject: Fixing a pat%constr bug. Thanks to Enrico for reporting. --- tactics/tacinterp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 693b382cac..59420e4e01 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -866,7 +866,7 @@ and interp_intro_pattern_action ist env sigma = function let sigma,l = interp_intro_pattern_list_as_list ist env sigma l in sigma, IntroInjection l | IntroApplyOn (c,ipat) -> - let c = fun env sigma -> interp_constr ist env sigma c in + let c = fun env sigma -> interp_open_constr ist env sigma c in let sigma,ipat = interp_intro_pattern ist env sigma ipat in sigma, IntroApplyOn (c,ipat) | IntroWildcard | IntroRewrite _ as x -> sigma, x -- cgit v1.2.3 From 5ad28372f001acbc562e1d095728cdb8a131938c Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 10 Dec 2015 18:26:08 +0100 Subject: Add tactic native_cast_no_check, analog to vm_cast_no_check. --- tactics/coretactics.ml4 | 4 ++++ tactics/tactics.ml | 4 ++++ tactics/tactics.mli | 1 + 3 files changed, 9 insertions(+) (limited to 'tactics') diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index e909a14c9e..92d4960a7c 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -42,6 +42,10 @@ TACTIC EXTEND vm_cast_no_check [ "vm_cast_no_check" constr(c) ] -> [ Proofview.V82.tactic (Tactics.vm_cast_no_check c) ] END +TACTIC EXTEND native_cast_no_check + [ "native_cast_no_check" constr(c) ] -> [ Proofview.V82.tactic (Tactics.native_cast_no_check c) ] +END + TACTIC EXTEND casetype [ "casetype" constr(c) ] -> [ Tactics.case_type c ] END diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 536a10eaa7..131730ebc0 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1731,6 +1731,10 @@ let vm_cast_no_check c gl = let concl = pf_concl gl in refine_no_check (Term.mkCast(c,Term.VMcast,concl)) gl +let native_cast_no_check c gl = + let concl = pf_concl gl in + refine_no_check (Term.mkCast(c,Term.NATIVEcast,concl)) gl + let exact_proof c gl = let c,ctx = Constrintern.interp_casted_constr (pf_env gl) (project gl) c (pf_concl gl) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index b9a0184180..896b33727c 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -118,6 +118,7 @@ val intros_patterns : intro_patterns -> unit Proofview.tactic val assumption : unit Proofview.tactic val exact_no_check : constr -> tactic val vm_cast_no_check : constr -> tactic +val native_cast_no_check : constr -> tactic val exact_check : constr -> unit Proofview.tactic val exact_proof : Constrexpr.constr_expr -> tactic -- cgit v1.2.3