Radosław Rowicki

Combined induction scheme is broken for inductive types that are not truly mutually recursive

3

### Description of the problem The `Combined Scheme` is very inconsistent and sometimes crashes. Several examples: ```coq Inductive A := a : A with B := b : B. Scheme...

Asserting outputs of vernacular commands and tactics

9

Render: Referenced issue: rocq-prover/rocq#20688

Debugging generalized rewriting tactics

1

Render: Referenced issue: rocq-prover/rocq#9285

`Capture Output` control and `Test Output` command for asserting outputs of vernac commands.

1

This is a very early draft/POC. Some stuff might be (is) totally wrong. Publishing it to get some preliminary feedback and how-tos. Design discussion there: https://github.com/rocq-prover/rfcs/pull/107 ----- Example: ```coq Capture...