diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-06-16 14:09:25 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-06-16 14:09:25 +0200 |
| commit | f9a619753644ba8e0f0ca1218396c8efee52b544 (patch) | |
| tree | de3c578430f5760ba862cc2d57a16fbcabc3c9f6 /plugins/setoid_ring/Ring_tac.v | |
| parent | da92254c786a62d05a66f12b4e8e01171e171e3c (diff) | |
Remove inappropriate comment.
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 77863edc1..fc02cef10 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 |