The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Is it possible to register a coercion with Coq without having it actually insert any function?  For example, if the types [A] and [B true] are judgmentally equal, is there any way to tell Coq that when it has an [A] and wants a [B ?n] for ?n an evar, it should instantiate ?n with true?  I have tried [Coercion silly (x : A) : B true := x], but this will block rewriting (because it gets in the way of pattern matching).

Thanks,

Jason