Jason Gross

> That would be a bug. Have you filed an issue? If I had known about it, I would have looked at it earlier. Not for this in particular, but...

To be clear, I'd very much like the ability to interleave Ltac2 debugging with Ltac1 debugging (and similarly with debugging invocations of cbv nested inside tactics, etc).

There is also proviola, which may not be what you want, but let's you display the Coq state on hover. See the HoTT wiki for an example: http://hott.github.io/HoTT/proviola-html/HoTT.Fibrations.html

I think I need @herbelin 's help in how to factor notations so that they work: ```coq Require Import Coq.Lists.List. Declare Scope seq_scope. Open Scope seq_scope. Notation "[ 'seq' E...

> reformulate `pred_of_simpl (@pred_of_argType T)` under a form referring to `x : T` rather than to only `T` in notation @herbelin What about using the `match` trick for substitution to...

> We need `x : T` to occur in position of binder so that when substituted with something such as `'pat` it continues to make sense, What about the equivalent...

(Of course the `match` form will never be used for printing, I don't know if that is an issue)

> What about the equivalent of `(fun A (a : A -> True) => A) _ (fun x : T => I)`? ```coq Notation "'type_of' x" := match _, (fun...

Updated PR, seems to be working

Two issues seem to arise: 1. This change is incompatible with Coq 8.11 and Coq 8.12. With mathcomp be dropping support for these versions on master anytime soon? 2. multinomials...