The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT inria.fr>]

Hi,

  I had never thought of this and this might be a bad idea, but what if we said that applying:

Hint Extern 0 (Proper (le ==> _ ==> impl) le) => fail 1 : typeclass_instances.

Would make the rest of the list of applicable hints be ignored (I.e backtracking on the previous goal). [fail n] could backtrack to a specific depth of the search tree I think, and we could have fail oo too. [fail 0] would retain its meaning, which is to try to apply the next available hint.

Cheers,
-- Matthieu

Le mer. 1 juin 2016 à 21:45, Paul A. Steckler <steck AT stecksoft.com> a écrit :

On Wed, Jun 1, 2016 at 12:43 PM, Jason Gross <jasongross9 AT gmail.com> wrote:
>  This means I need to be extremely careful to not put any lemmas in my rewriting databases which can utterly fail to be respected by any other relation (so any facts about [le] or [lt] are right out).

Maybe there are some heuristics to be applied here, since we can't
identify such lemmas in general.

-- Paul