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/equality.ml | |
| parent | 5003953d45ea0e780cd50bb9d6521799adf18079 (diff) | |
| parent | 711b9d8cdf6e25690d247d9e8c49f005527e64e2 (diff) | |
Merge PR #915: Fix rewrite in * side conditions
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 4 |
1 files changed, 2 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 |