Ssreflect Users Discussion List

[Florent Hivert <>]

      Dear Georges and Emilio,

On Mon, Feb 15, 2016 at 06:09:02PM +0000, Georges Gonthier wrote:
> This ensures the definition if never unfolded by the type checker
> heuristics, but unfortunately this is not sufficient to block the compute
> strategy - eager definition expansion with strong call-by-value. Hence the
> compute in your proof attempts to create a huge term.

Thanks both of you for your detailed answer. I know only very few about Coq's
internal so I'm not sure to completely understand everything. Anyway It seems
that Cohen & al. is something I can read about the subject...

> IMVHO, even if hacky, this approach didn't work out too bad. I could send
> you some drafty code off-list if you are interested.

Please do !

Florent