The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 17/08/2017 15:45, Robbert Krebbers wrote:
> I noticed that when enabling primitive projections the performance
> programs go away entirely in my small examples (all uses of apply will
> fail within ~0.00 seconds). Unfortunately, in my actual development,
> primitive projections seem to cause other problems: canonical structure
> inference no longer works when they are enabled, and the Ssreflect
> rewrite tactic to fail unexpectedly. Are these problems known?

Also, while I'm thinking about this, could you report this on the bug
tracker with self-contained reproducible examples? Primitive projections
ought to work out-of-the-box for canonical structures and the like.

(Notwithstanding the fact that the Coq bugzilla is currently down.)

PMP

Attachment: signature.asc
Description: OpenPGP digital signature