diff options
Diffstat (limited to 'plugins/setoid_ring/Ring_tac.v')
-rw-r--r-- | plugins/setoid_ring/Ring_tac.v | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v index fc02cef10..d488ef140 100644 --- a/plugins/setoid_ring/Ring_tac.v +++ b/plugins/setoid_ring/Ring_tac.v @@ -427,19 +427,23 @@ 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; + 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. - + 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 |