diff options
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/Ring_tac.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v index d488ef140..329fa0ee8 100644 --- a/plugins/setoid_ring/Ring_tac.v +++ b/plugins/setoid_ring/Ring_tac.v @@ -429,6 +429,13 @@ Tactic Notation "ring_simplify" constr_list(rl) "in" hyp(H):= set (g:= G); generalize H; ring_lookup (PackRing Ring_simplify) [] rl t; + (* + Correction of bug 1859: + we want to leave H at its initial position + this is obtained by adding a copy of H (H'), + move it just after H, remove H and finally + rename H into H' + *) let H' := fresh "H" in intro H'; move H' after H; @@ -442,6 +449,13 @@ Tactic Notation "ring_simplify" "["constr_list(lH)"]" constr_list(rl) "in" hyp(H set (g:= G); generalize H; ring_lookup (PackRing Ring_simplify) [lH] rl t; + (* + Correction of bug 1859: + we want to leave H at its initial position + this is obtained by adding a copy of H (H'), + move it just after H, remove H and finally + rename H into H' + *) let H' := fresh "H" in intro H'; move H' after H; |