diff options
Diffstat (limited to 'plugins/setoid_ring')
-rw-r--r-- | plugins/setoid_ring/Ring_tac.v | 34 |
1 files changed, 26 insertions, 8 deletions
diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v index fc02cef10..329fa0ee8 100644 --- a/plugins/setoid_ring/Ring_tac.v +++ b/plugins/setoid_ring/Ring_tac.v @@ -427,19 +427,37 @@ Tactic Notation "ring_simplify" constr_list(rl) "in" hyp(H):= let t := type of H in let g := fresh "goal" in set (g:= G); - generalize H;clear H; + generalize H; ring_lookup (PackRing Ring_simplify) [] rl t; - intro H; + (* + 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; + clear H;rename H' into H; unfold g;clear g. -Tactic Notation - "ring_simplify" "["constr_list(lH)"]" constr_list(rl) "in" hyp(H):= +Tactic Notation "ring_simplify" "["constr_list(lH)"]" constr_list(rl) "in" hyp(H):= let G := Get_goal in let t := type of H in let g := fresh "goal" in set (g:= G); - generalize H;clear H; + generalize H; ring_lookup (PackRing Ring_simplify) [lH] rl t; - intro H; - unfold g;clear g. - + (* + 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; + clear H;rename H' into H; + unfold g;clear g.
\ No newline at end of file |