aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/setoid_ring/Ring_tac.v2
1 files changed, 1 insertions, 1 deletions
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")]).