Jason Gross

instantiate permits ill-typed instantiations when the term is bound by Ltac

2

#### Description of the problem ```coq Goal forall (f : False -> False), exists x : True -> False, forall (v : False), x I = f v. intro F....

#### Description of the problem `instantiate` is currently crippled with regards to automation. I can write ```coq Goal exists n : nat, n = n. eexists ?[n]. instantiate (n:=1). ```...

`vm_compute` should not reduce in evar substitutions

1

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

#### Description of the problem ```coq Goal forall x : nat, let y := x in exists z : nat, let w := z in w = w -> True....

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

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

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

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

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

coq binaries from CI are basically unusable without docker

4

I'd like to reuse CI artifacts when debugging failures. It used to be the case that I could just download the artifacts and unpack them, and coqc would run. Since...