Ssreflect Users Discussion List

[Enrico Tassi <>]

On Thu, Nov 07, 2013 at 11:06:47AM -0500, Maxime Dénès wrote:
> Hello Georges and Enrico,
> 
> Is the flag you mention "default_no_delta_unify_flags" in
> unification.ml, which sets "modulo_betaiota" to false but leaves the
> default "modulo_eta" (true)?

Exactly

> I can relay the problem on coqdev if you wish, so that we know if
> this was intended for some reason or if a record field update was
> simply forgotten (and get it fixed, in this case).

As you prefer... but fixing it now may force users to (un)fix their
script again if a new pl is released (assuming that have ported them to
the current 8.4)...

> As for the change of behavior of the cooking, did you trace it?

Arnaud just removed the beta normalization at the end of section.

Ciao
-- 
Enrico Tassi