Ssreflect Users Discussion List

[Cyril Cohen <>]

Hi Maxime,

On 28/12/2011 10:19, Maxime Dénès wrote:
> Would you have any suggestion ? Could I make some definitions opaque to 
> have a
> more tractable situation ? Is that yet another symptom indicating that Coq's
> kernel should cache rejected conversions ?

There is currently a problem in poly (which we uncovered a few days ago with
Pierre-Yves) with the locking of (add|opp|mul)_poly. This could be the reason 
for
this slowness. Let me commit the fix and try again when it's done, please.

best seasonal wishes
-- 
Cyril Cohen