coq

coq copied to clipboard

[dune] [test-suite] Port the test suite to Dune

35

This is an in-progress PR to port the test suite to Dune. Main design principles are: - use the standard `runtest` infrastructure, and declare all the dependencies correctly so the...

ejgallego

Deactivation of notations: providing vernac syntax, vo registration and support for deactivation of abbreviations

37

**Kind:** feature This extends #703 on selective deactivation of notations by adding: - concrete syntax for deactivation/reactivation - registration in vo files - support for deactivation of abbreviations Added: Now...

herbelin

Extend .mailmap to eliminate some duplicates in `git shortlog -se`

13

If there was already an account in .mailmap, I preferred the one already present. If there was not, I preferred whichever account had more commits. Additions I'm unsure about: -...

JasonGross

Fixes #16303: evar defined before its instance was checked, leading to error message trying to unexpectingly display an already defined evar

40

This improves commit 26a5b65df from PR #14797. Fixes #16303 - [x] Added / updated **test-suite**. - [x] Added **changelog**.

herbelin

#### Description of the problem ```coq Ltac foo := match goal with H := context[nat] |- _ => idtac end. Set Printing All. Print Ltac foo. (* Ltac foo :=...

JasonGross

#### Description of the problem ```coq Fixpoint fact (n : nat) := match n with 0 => 1 | S n' => n * fact n' end. Goal forall m...

JasonGross

#### Description of the problem Like #16358 ```coq Fixpoint fact (n : nat) := match n with 0 => 1 | S n' => n * fact n' end. Goal...

JasonGross

performance of [field_simplify_eq] is linear when it should be constant

22

Note: the issue was created automatically with bugzilla2github tool Original bug ID: BZ#4810 From: @JasonGross Reported version: 8.6 CC: @barras, @silene, @herbelin, @mattam82, @ppedrot

coqbot

jfehrle

`Ltac2.Constr.in_context` should accept a list (or array) of constrs (or have a variant that does so)

2

As I understand it, https://github.com/coq/coq/blob/27c8770d4e92a763c382e0ec2585d04eaa95c49f/user-contrib/Ltac2/Constr.v#L92-L95 https://github.com/coq/coq/blob/27c8770d4e92a763c382e0ec2585d04eaa95c49f/plugins/ltac2/tac2core.ml#L708-L738 is linear in the size of the existing context, and this means that folding it over a list results in quadratic behavior. I'd like...

JasonGross