From 6458868b7ba2eb04cad7bf670dda6ba4f01f7c80 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 5 Aug 2014 16:49:13 +0200
Subject: Ring: prevent an error message to show in case of success.

Since [idtac] can, now, be used even if no goal is left, this error message which assumed that the goal was still open would run at every call of the [ring] tactic. Which lead to comically many nonsensical messages on the console during Coq's compilation.
---
 plugins/setoid_ring/Ring_tac.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v
index 8bb44ecbc7..77863edc1e 100644
--- a/plugins/setoid_ring/Ring_tac.v
+++ b/plugins/setoid_ring/Ring_tac.v
@@ -351,7 +351,7 @@ Ltac Ring RNG lemma lH :=
       || fail "typing error while applying ring");
     [ ((let prh := proofHyp_tac lH in exact prh)
         || idtac "can not automatically prove hypothesis :";
-           idtac " maybe a left member of a hypothesis is not a monomial")
+           [> idtac " maybe a left member of a hypothesis is not a monomial"..])
     | vm_compute;
       (exact (eq_refl true) || fail "not a valid ring equation")]).
 
-- 
cgit v1.2.3