From b4aba0a95493e7dd9f9bbfcaeade4015b697cd00 Mon Sep 17 00:00:00 2001 From: Julien Forest Date: Tue, 1 Aug 2017 11:53:58 +0200 Subject: adding a comment to explain the change --- plugins/setoid_ring/Ring_tac.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'plugins/setoid_ring') 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; -- cgit v1.2.3