The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 05/06/2014 09:41 PM, Jonathan wrote:

After doing a git pull of the trunk - which included a large number of changes around universe polymorphism (changes through 2014-05-06), proofs that were working previously are now failing.  I don't think any of these proofs had much if anything to do with universe polymorphism.

I'll follow up with some test cases, which I'll first try to factor out of the surrounding code...

-- Jonathan

Here's one new failure, with a workaround:

Require Export Coq.Classes.RelationClasses.

Section defs.
  Variable A : Type.
  Variable lt : A -> A -> Prop.
  Context {ltso : StrictOrder lt}.

  Goal forall (a : A), lt a a -> False.
  Proof.
    intros a H.
    contradict (irreflexivity H). (*now fails, but the following still works:*)
    contradict (@irreflexivity _ lt _ _ H).
  Qed.
End defs.