Jason Gross

> Propositional realization guarantees consistency Consistency with the base theory of Coq but not with consistent extensions, right? E.g., propositional realization is not enough to remain consistent with univalence, I...

Consider: ```coq Definition foo (x y : nat) := existT (fun T => T) bool true. Rewrite Block := bar : nat -> nat -> { T : Type &...

My wish is that OCaml tactics should not be special, or at least should be as unspecial as possible. If an OCaml tactic can resolve it's flags at internalization time,...

@herbelin to the call site of the tactic being defined. Alternatively, I'd like something like ``` LtacWithOptions(options) myrewrite lem := with_options options rewrite lem. ``` And then if `myrewrite` is...

Are these two the same? ``` Ltac myrewrite lem := version runtime in rewrite lem. Ltac myrewrite87 lem := version 8.7 in myrewrite lem. ``` And ``` Ltac myrewrite87 lem...

This issue is not stale, as can be easily determined by visiting the link in the report.

This issue is still open, as is obvious from 10 seconds of inspection. Why has there been no response from the team for six months on this very simple issue?

It's been almost two years and the only response I've gotten to this issue is from @stale[bot]

It makes a tiny bit of sense, but I don't have a good idea about how to construct a smaller test case, nor a really good understanding of what's happening...

I'm not sure... I bet @mikeshulman would know (or would know who to ask).