diff options
| author | Maxime Dénès | 2018-03-04 16:27:54 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-04 16:27:54 +0100 |
| commit | ed05111e048e864c63c2e21b8ebac675a80dc464 (patch) | |
| tree | 47e7bb219ba43e901b2bfc3791e80f161246dd54 /tactics | |
| parent | 5003953d45ea0e780cd50bb9d6521799adf18079 (diff) | |
| parent | 711b9d8cdf6e25690d247d9e8c49f005527e64e2 (diff) | |
Merge PR #915: Fix rewrite in * side conditions
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 9a1ac768c7..32563d9ffc 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 e7da17cff1..0cc0001c1c 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 c5d5c8c123..a3bc4707ea 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 |