Adapt to Coq PR #19404: an algebra of types for the instances of notation variables

LPCIC / coq-elpi

Coq plugin embedding elpi

GNU Lesser General Public License v2.1

137 stars 50 forks source link

Open herbelin opened 2 months ago

herbelin commented 2 months ago

This PR is in preparation of coq/coq#19404 which introduces an algebra of types for the instances of notation variables.

To be merged synchronously.

gares commented 2 months ago

Please use optcomp in order to make the pr work on 8.19 and 8.20