The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Thu, Jun 04, 2015 at 11:29:27AM +0200, Ralf Jung wrote:
> I played around with SimplIsCbn, but it seems that ssreflect's "/=" will
> still call the old simpl. At least, "move=>/=" does not behave like
> "cbn" even with SimplIsCbn set. Is there any way to tell Ssreflect to
> also use cbn?

Unfortunately not, "simpl" is hard coded in ssreflect 1.5.
Next version will honor SimplIsCbn.

Best,
-- 
Enrico Tassi