search

LPCIC / coq-elpi

Coq plugin embedding elpi
GNU Lesser General Public License v2.1
139 stars 51 forks source link

wish: coq.env.add-* could typecheck by default #710

Open gares opened 4 weeks ago

gares commented 4 weeks ago

to improve error experience, since forgetting it may just give a universe error that is not very clear