Jason Gross

README should document cygwin interaction on Windows

9

IMHO, the readme should document the answers to the following questions: If I want to use cygwin and setup-ocaml on Windows, what's the workflow? In particular: - Do I install...

packages with a validate target should have a `run-test`

5

Apparently [opam has `--with-test`](https://opam.ocaml.org/doc/Manual.html#opamfield-run-test). The doc on making opam packages should suggest filling this field, and the packages which have validate targets available should get this field.

This is a work in progress; is someone from @coq/ltac2-maintainers willing to help me complete the OCaml side of this? - [ ] Added / updated **test-suite**. (is this needed?)...

Neglecting to call `Ltac2.Constr.Unsafe.check` results variously in "Ill-typed evar instance" or assertion failures on `exact`

4

#### Description of the problem I'd like some help figuring out what's going on here. Roughly the thing going on is that I'm creating something roughly analogous to `@id _...

Put Ltac2.Bool notations in a separate module

2

This way we can import them separately from the boolean operators. We name it `BoolNotations` after `Coq.Lists.List.ListNotations`. - [ ] Added / updated **test-suite**. (nothing to do?) - [x] Added...

Anomaly "Evar ?X3577 was not declared. on `transparent_abstract`(?)

3

#### Description of the problem I've no idea what's going on here, maybe someone with more understanding of the code can make an example that's shorter than 12086 lines (or...

- [ ] Added / updated **test-suite**. (is this needed?) - [x] Added **changelog**. - [ ] Added / updated **documentation**. (no doc to update?)

We mirror the List functions. - [ ] Added / updated **test-suite**. (should I?) - [x] Added **changelog**. - [ ] Added / updated **documentation**. (is there any to update?)

#### Description of the problem I'd like to have something at least as featureful as either Coq's scope system or OCaml's infix system for Ltac2 notations. In particular, I'd like...

- [ ] Added / updated **test-suite**. (should I?) - [x] Added **changelog**. - [ ] Added / updated **documentation**. (is there any to add?)