From f9a619753644ba8e0f0ca1218396c8efee52b544 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Thu, 16 Jun 2016 14:09:25 +0200
Subject: Remove inappropriate comment.

---
 plugins/setoid_ring/Ring_tac.v | 2 --
 1 file changed, 2 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 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
-- 
cgit v1.2.3