The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi Randy,

  You still need to install the plugin, it's not part of Coq proper. Code is 
available on github that works with the current trunk version (the coq-trunk 
branch). The README there should be sufficient to get you started. Otherwise 
it's a bug. And there will be an official release with 8.4.

Hope this helps,
-- Matthieu

Le 27 sept. 2011 à 10:05, Randy Pollack 
<rpollack0 AT gmail.com>
 a écrit :

> My first attempt to use Equations.  The Tutorial
> (mattam.org/research/coq/equations-intro.html) says : "... requiring
> no prior knowledge of the tool. We start our Coq primer session by
> importing the Equations module.
> 
>  Require Import Equations.
> 
> Coq (8.3pl2) says "Error: Cannot find library Equations in loadpath".
> 
> Any help is appreciated.
> 
> Randy