ring

The conclusion of the current sequent must be an equality over Coq's real numbers that can be proved using the ring properties of the real numbers only.

It closes the current sequent veryfying the equality by means of computation (i.e. this is a reflexive tactic, implemented exploiting the "two level reasoning" technique).

None.