FissoreD / coq-elpi

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

Scope check is too expensive #3

Open FissoreD opened 2 months ago

FissoreD commented 2 months ago

Scope check triggers the same link each time it is called if the link has unification variables. This call is unnecessary if no pruning is performed.

A solution may be to do scope check only if the list of names in the scope is shrinked