Top

Module mathcomp.test_suite.test_ring_error

From mathcomp Require Import ssreflect ssralg ring_tactic.


Goal forall (R : comRingType) (a : R), (a + a = a)%R.

Proof.

move=> R a.
Fail ring. (* prints Not a valid ring equation. *)
ring || idtac "elpi-tactic failure caught by ltac".
Abort.