Ssreflect Users Discussion List

[Enrico Tassi <>]

On Sat, Sep 14, 2013 at 04:11:18PM +0000, t x wrote:
>   ## now, it appears to inifnite loop on:
> 
>   coqc  -q  -I src -R theories Ssreflect   theories/finfun

It is a problem Beta also encountered, but we did not manage to pinpoint
the problem IIRC.

Mtac patches evarconv.ml, and because of that a rewrite step in finfun
loops.  The patch looks fine to me, so it could be an explicit unbounded
iteration in the script (like rewrite !foo) that is terminating because
stock evarconv.ml fails for a bad reason, and Beta's optimization makes
it succeed (correctly) forever.

I'm sorry but I don't find in my mailbox a message, in the exchange
I had with Beta, with an actual solution.
It could be as easy as finding the line in which it loops and changing
it slightly putting a bound on the iteration, but I don't have mtac at
hand...

Cheers
-- 
Enrico Tassi