diff options
Diffstat (limited to 'plugins/setoid_ring/Ring_tac.v')
| -rw-r--r-- | plugins/setoid_ring/Ring_tac.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v index 77863edc..fc02cef1 100644 --- a/plugins/setoid_ring/Ring_tac.v +++ b/plugins/setoid_ring/Ring_tac.v @@ -422,8 +422,6 @@ Tactic Notation (at level 0) let G := Get_goal in ring_lookup (PackRing Ring_simplify) [lH] rl G. -(* MON DIEU QUE C'EST MOCHE !!!!!!!!!!!!! *) - Tactic Notation "ring_simplify" constr_list(rl) "in" hyp(H):= let G := Get_goal in let t := type of H in |