The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Fri, Aug 21, 2015 at 01:28:53PM +0000, Ilya Sergey wrote:
> However, adding "Polymorphic" to the first definition makes the last
> rewrite of the proof break with the following error:
> 
> Error: The RHS of G
>     (foo f x)
> does not match any subterm of the goal

Thanks for the bug report, indeed there is a little bug concerning
universe polymorphic constants.  The fix is here:

  
https://github.com/math-comp/math-comp/commit/14c940b332512f313b0b80acd6a17f80721b32fc

The fix will be part of the next SSR release.  It should apply cleanly to
version 1.5 for for Coq 8.5 beta 2.

Unfortunately we don't have a test suite that includes Universe
Polymorphic code, so ... your testing is very welcome.

Best wishes,
-- 
Enrico Tassi