diff options
| author |  Julien Forest <julien.forest@ensiie.fr> | 2017-08-01 00:07:12 +0200 |
|---|---|---|
| committer | Julien Forest <julien.forest@ensiie.fr> | 2017-08-01 00:07:12 +0200 |
| commit | 11ab8eb6c7f6475de03c7ce258bf48d461d5892f (patch) | |
| tree | 0075cbbae514a54dd4e4847aee0a1aea0f844d31 /plugins/setoid_ring | |
| parent | 17f37f42792b3150fcebb6236b9896845957b89d (diff) | |
solving b1859
Diffstat (limited to 'plugins/setoid_ring')
| -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 |