The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le lundi 26 novembre 2012 à 06:10 +0100, Hugo Herbelin a écrit :

> If we restrict proof-irrelevance to non-recursive-singleton (Acc) and
> no-with-indices-singleton (eq) propositions (*), then we have to
> forbid also propositional variables, since they may get eventually
> substituted by one of these propositions we want to exclude.

I thought I was starting to grasp what the situation is about, but
looking at your last comment, I am not so sure anymore. It seemed to me
that the only case that mattered when checking convertibility was
whether surjective pairing could be applied to the argument of a
match/fix. Thus propositional variables should have been fine, since
their values are never matched upon. What are the other cases that could
happen?

Best regards,

Guillaume