coq

coq copied to clipboard

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...

JasonGross

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

JasonGross

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

JasonGross

#### 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...

JasonGross

[configure] [coqide] Put coqide config in its own file.

1

Follow up of #16512 , eventually coqide should have its own configure script.

ejgallego

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

JasonGross

- [ ] Added / updated **test-suite**. (is this needed here, since we're just exposing unerlying ml primitives?) - [x] Added **changelog**. - [ ] Added / updated **documentation**. (is...

JasonGross

- [ ] Added / updated **test-suite** (do we need it?) - [x] Added **changelog**. - [ ] Added / updated **documentation**. (do we need it?)

JasonGross

ejgallego

Allow Ltac2 notations from within Ltac1

12

This is preliminary work to check that the design aligns with the requirements of the people who asked for this feature. This PR adds a new Ltac2 vernacular command of...

ppedrot