search

LPCIC / coq-elpi

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

[coq.TC.get-inst-prio] new get-inst-prio (#716) #717

Closed FissoreD closed 13 hours ago

FissoreD commented 2 days ago

With the new push, I'm not sure the tc-priority remains relevant, orelse, if we want to keep this piece of information we need to reuse the old algorithm to know if the instance has a UserGiven priority.

Note that in that case, I'm not sure how to know if a hint (added with hint resolve) has a UserGiven priority

gares commented 1 day ago

In these cases I think having the exception carry the found value is less cumbersome.

Otherwise looks good.