From 11ab8eb6c7f6475de03c7ce258bf48d461d5892f Mon Sep 17 00:00:00 2001 From: Julien Forest Date: Tue, 1 Aug 2017 00:07:12 +0200 Subject: solving b1859 --- plugins/setoid_ring/Ring_tac.v | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) (limited to 'plugins/setoid_ring/Ring_tac.v') 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 -- cgit v1.2.3