Fix after decide equality is able to keep proofs in arguments in Prop.

[herbelin]

Hi,

Coq 8.7 shall come with a fix to decide equality which makes it working better (even though more progresses are expectable). However, this improvement breaks topology.

The attached patch allows to compile topology with 8.7. However, the fix is not compatible with 8.6. May I let you decide if you prefer preparing your own patch so as to be compatible over both 8.6 and 8.7 at the same time, or whether you prefer to have disjoint versions.

Note that we can also provide various different ways to support compatibility over different versions. For instance, the question of possibly providing Set Version 8.6./Unset Version 8.6. commands around parts of code that would work only in 8.6 has been considered, though no final decision has been taken yet. Don't hesitate to tell your point of view as a user, if you have one.

[bmsherman]

Thanks! I'll try to take a look at this in the coming days. I think I will just use decidable quality explicitly in the cases where it works in both 8.6 and 8.7 and use the manual derivation elsewhere (rather than just using try).

[bmsherman]

I made a small change with commit c7bccde to just stop using the decidable equality tactic. Apparently on 8.6 it was only solving decidable equality on False, which I can easily do myself! This should work for both 8.6 and 8.7, but I haven't gotten the chance to test with the latest version of coq-dev. The build with coq-dev is erroring in Travis CI, I think due to a failure to install CoRN, so I can't tell. But this seems like a safe change and ought to allow compilation on both 8.6 and 8.7.

As a note, I believe that the branch that you're tracking is ci, rather than master. Once I get evidence that I didn't break things with this change, I'll incorporate the change into ci so it works for you!