Order tactic fails when eq is defined in terms of le

[dfoxfranke]

Version

The Coq Proof Assistant, version 8.6.1 (November 2017)
compiled on Nov 5 2017 23:16:40 with OCaml 4.02.3

Operating system

Linux x86_64, NixOS 17.09

Description of the problem

Given an OrderTac module for T, I want to use the order tactic to prove

x, y : T
H : y < x -> False
______________________________________(1/1)
x <= y

But after order_prepare it ends up with

x, y : T
H : x <= y
H0 : ~ y == x
______________________________________(1/1)
False

which is not provable.

The trouble lies in my definition of eq x y as le x y /\ le y x and in the application of not_neg_eq at https://github.com/coq/coq/blob/a4043608f704f026de7eb5167a109ca48e00c221/theories/Structures/OrdersTac.v#L214. This application shouldn't succeed, but it does, because when apply is given a function of type A -> B /\ C, it'll "helpfully" add the necessary projection to unify with a goal of B. So in this case, not_neq_eq has type ~~y==x -> y==x, which unfolds to ~~y==x -> y <= x /\ x <= y, which undesirably unifies with the goal of x <= y.

This can be fixed by using simple apply rather than apply.