Ssreflect Users Discussion List

[Enrico Tassi <>]

On Sun, Aug 04, 2013 at 11:34:02AM +0200, Alain Lichnewsky wrote:
> Error message terminating make:
> 
> File "src/ssrmatching.ml4", line 889, characters 0-7:
> Parse error: Deprecated syntax, use EXTEND MyGramModule ... END instead

Right, the ssreflect plugin stopped working with recent camlp4 version.
The simplest fix is to install camlp5 and recompile Coq.

I'll try to make next release work with both parser engines, but I'm not
sure it will ever work (Coq has a hack to support camlp4 that
essentially installs a token filter to apply your patch on the fly.  I
may or may not be able to use it while building the plugin)

Cheers
-- 
Enrico Tassi