Jan-Oliver Kaiser

~~I should add that I am not using `autoapply` for actual production code but I do use it to for debugging and experimentation. For those purposes it would be great...

My initial analysis was wrong: this bug is not about autoapply (or about it behaving differently from typeclass search). This is actually a bug about typeclass search or, rather, the...

Any chance this bug could be fixed? We now have two features in our code base that are blocked on this. And I suspect the more we try to unify...

I assume the partial application in QuickChick is from coq-ext-lib. Candidates include: 1) https://github.com/coq-community/coq-ext-lib/blob/73fa2d83a075adedc65c1f5888d7f688f9e31f0c/theories/Data/Monads/ListMonad.v#L7 2) https://github.com/coq-community/coq-ext-lib/blob/73fa2d83a075adedc65c1f5888d7f688f9e31f0c/theories/Data/List.v#L123 There might be more list monads in there.

Let's go with `[email protected]`. Given my current progress on finishing my PhD that one will stay alive for a long long time even without a redirect..

This comment here is very related: https://github.com/coq/coq/blob/master/plugins/ltac2/tac2ffi.ml#L249 The backtraces exist whenever `Set Ltac2 Backtrace` is enabled but they are thrown away whenever the exception passes the OCaml/Ltac2 boundary. (Raising an...

I think that error does not originate in Ltac2 but rather in Ltac1's `constr:()`. `'` in Ltac2 is `open_constr:()` IIRC and that accepts `_` just fine: ``` Succeed ltac2:(let t...

No. You can only get the Ocaml backtrace. It would be an amazingly useful feature!

I personally am entirely used to these arguments appearing in pretty much random orders and I have mostly given up trying to remember which language does it which way around....

This is maybe slightly off-topic but the only converting between Ltac2 and OCaml I've done so far was to move performance-critical Ltac2 code to OCaml. My experience has been that...