The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I like it. It would be nice to put the behavior behind a flag, for compatibility.

Unfortunately, this won't help until I manage to get bedrock ported to Coq 8.5

On Thu, Jun 2, 2016, 3:23 AM Matthieu Sozeau <matthieu.sozeau AT inria.fr> wrote:

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