jim-portegies

#### Description of the problem I am getting a number of 'anomalies'. The easiest example I could think of producing an error for me is the following. ``` From Ltac2...

One way of structuring proofs in Coq is to use bullets and braces. This behavior can be enforced by ```Set Default Goal Selector "!".``` However, it seems that errors thrown...