Library Coq.Compat.Coq85


Compatibility file for making Coq act similar to Coq v8.5
Any compatibility changes to make future versions of Coq behave like Coq 8.6 are likely needed to make them behave like Coq 8.5.
Require Export Coq.Compat.Coq86.

We use some deprecated options in this file, so we disable the corresponding warning, to silence the build of this file.



The resolution algorithm for type classes has changed.

Allow silently letting unification constraints float after a "."