The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Le 07/10/2010 13:59, Pierre Casteran a écrit :
> Hi Thomas,
>
>
>  In coq's doc, there is a mention "The tactic must be loaded by 
> Require Import Ring. The ring structures must be declared with the Add 
> Ring command (see below). The ring of booleans is predefined"

I was mistaken by the fact that requiring Arith or ZArith allows you to 
use directly ring and
ring_simplify, but if you require Bool, you *have* to require Ring too 
(at least in 8.2pl1).

This dissymetry was the origin of my questions. Sorry for the spam.


Pierre