diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/setoid_ring/Ring_tac.v | 2 |
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")]). |
