search

mattam82 / Coq-Equations

A function definition package for Coq
http://mattam82.github.io/Coq-Equations
GNU Lesser General Public License v2.1
223 stars 44 forks source link

Remove a good part of the sources of abusive typing #606

Closed ppedrot closed 3 months ago

ppedrot commented 3 months ago

We carefully infer the minimal amount of constraints instead of unconditionally typing stuff on sight. There are still a few instances of useless typing but they are more tricky. (The next one on my radar is Simplify.solution).

This PR has been tested on MetaCoq. I'll try to get a bench running on it when the Coq workers are under a reasonable load.

ppedrot commented 3 months ago

@mattam82 I'm merging this, CI is green an metacoq is compiling so it's probably safe.