Robbert Krebbers

FWIW: I think an option to control backtracking would be super useful. I recently noticed that some failing tactics in Iris are excessively slow because Coq is backtracking like crazy,...

> Ignorance of that use case I suppose :) It seems this could be linked to mode declarations. Linking this to mode declarations would be a great idea. Basically, often...

So, to get this clear: there are two common ways in which backtracking may appear: 1. An instance `C x y → D y → E x y` where `y`...

I'm not very convinced that the current `Set Typeclasses Unique Instances` is useful, but regardless, it would be good if the documentation were improved. https://github.com/coq/coq/pull/7661 sounds like a something that's...

Any idea if #7661 covers scenario 1? If so, I think I would be happy. Nit: If it does, it appears we have to say `NonBacktracking` for each instance, which...

An interesting observation related to @RalfJung's previous point: - `Hint Mode` is currently at the the level of classes. - `NonBacktracking` is currently at the level of instances. Arguably, you...

@SkySkimmer This example seems to make a lot of sense. I will try #7661 on Iris once it's rebased on Coq master.

Awesome. I will try this out after the POPL deadline is passed.

Sorry for the very delayed response. Deadlines, switching jobs, trying to buy a house, and vacation caught up (and are still catching up) on me. I tried to implement to...

I wonder if the following trick would be sound: ``` Axiom ptr_eq : forall {A B} (x y : A) (eq : x = y -> unit -> B) (neq...