diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-07-21 13:43:31 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-01 12:05:39 +0100 |
| commit | 711b9d8cdf6e25690d247d9e8c49f005527e64e2 (patch) | |
| tree | 5a19ec52e7a510a456195d3814958abc33e47f73 /tactics | |
| parent | f726e860917b56abc94f21d9d5add7594d23bb6d (diff) | |
Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".
Noticed by Sigurd Schneider.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 4 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 6 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 1 |
3 files changed, 9 insertions, 2 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 9a1ac768c..32563d9ff 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -533,7 +533,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl = let rec do_hyps_atleastonce = function | [] -> tclZEROMSG (Pp.str"Nothing to rewrite.") | id :: l -> - tclIFTHENTRYELSEMUST + tclIFTHENFIRSTTRYELSEMUST (general_rewrite_ebindings_in l2r AllOccurrences false true ?tac id c with_evars) (do_hyps_atleastonce l) in @@ -549,7 +549,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl = end in if cl.concl_occs == NoOccurrences then do_hyps else - tclIFTHENTRYELSEMUST + tclIFTHENFIRSTTRYELSEMUST (general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars) do_hyps diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index e7da17cff..0cc0001c1 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -408,8 +408,14 @@ module New = struct Proofview.tclIFCATCH t1 (fun () -> tclDISPATCH (Array.to_list a)) (fun _ -> t3) + let tclIFTHENFIRSTELSE t1 t2 t3 = + Proofview.tclIFCATCH t1 + (fun () -> tclEXTEND [t2] (tclUNIT ()) []) + (fun _ -> t3) let tclIFTHENTRYELSEMUST t1 t2 = tclIFTHENELSE t1 (tclTRY t2) t2 + let tclIFTHENFIRSTTRYELSEMUST t1 t2 = + tclIFTHENFIRSTELSE t1 (tclTRY t2) t2 (* Try the first tactic that does not fail in a list of tactics *) let rec tclFIRST = function diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index c5d5c8c12..a3bc4707e 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -210,6 +210,7 @@ module New : sig val tclIFTHENELSE : unit tactic -> unit tactic -> unit tactic -> unit tactic val tclIFTHENSVELSE : unit tactic -> unit tactic array -> unit tactic -> unit tactic val tclIFTHENTRYELSEMUST : unit tactic -> unit tactic -> unit tactic + val tclIFTHENFIRSTTRYELSEMUST : unit tactic -> unit tactic -> unit tactic val tclDO : int -> unit tactic -> unit tactic val tclREPEAT : unit tactic -> unit tactic |