search

FissoreD / coq-elpi

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

Always eta-contract solution #13

Open FissoreD opened 3 months ago

FissoreD commented 3 months ago

Instead of doing eta-contract on the solution in elpi, eta contract should be done in the coq-elpi backend after the run of the elpi program