diff options
| author | Arnaud Spiwack | 2014-08-05 16:49:13 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-08-05 16:58:52 +0200 |
| commit | 6458868b7ba2eb04cad7bf670dda6ba4f01f7c80 (patch) | |
| tree | 181bc2a7c050cc33740dca176e080d8f24f23482 /plugins | |
| parent | 5f9b15657dacd258fbd9084424afd4aa96929f3f (diff) | |
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.
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")]). |