Adapt to coq/coq#11368 (Turn trailing implicit warning into an error)

coq / stdlib2

GNU Lesser General Public License v2.1

39 stars 9 forks source link

Adapt to coq/coq#11368 (Turn trailing implicit warning into an error) #19

Closed SimonBoulier closed 4 years ago

herbelin commented 4 years ago

This backward-compatible PR can be merged. Actually, Coq PR #11368 being now merged to Coq, it would be better to merge it without too much delay if possible in order to remain synchronous with Coq CI. Thanks in advance