vblot

Sorry if this is a naive question, but why should we use uip or go to sprop ? I think reducing `eqb_correct i i (eq_refl true)` to `eq_refl i` as...

Yes, that is what I had in mind. Is this complicated?

I see. OTOH there are already many operations on `int` so one more seems harmless to me, but I understand the kernel is not something you want to change every...

> Just to be clear, there is no other equality proof. I think it depends on the semantics of "equality proof". If by that you mean a term (without axioms)...

> 1. Decidable types have UIP. Thanks! I had forgotten about that one... But then it seems counter-intuitive to require the uip flag, since `int` is decidable.

> OK, I am being confusing, sorry about that. There are two meanings for UIP over a type `A`, > > * first the fact that given any equality type...

> > having an additional opcode of type `forall x y:int, option (x = y)` makes sense to me, assuming it is sufficient. > > This should be sufficient for...

> Please let us not replace a trivial opcode with a costly memory-allocating one. That said, having an additional opcode of type `forall x y:int, option (x = y)` makes...

> > > Please let us not replace a trivial opcode with a costly memory-allocating one. > > > One option would be to actually replace the current primitive `eqb`...