Jason Gross

Version-conditional vernacular

1

I'd like to have a vernacular modifier like `Comment Unless ( 8.16

[v8.0] Add support for `-h` and `--help` to configure

2

d8b4083b2e865d6ab32e3aa33fa7eb50fa9c901f added a usage function without adding support for calling it. This will allow my scripts that configure multiple versions of Coq to work more fluently.

https://github.com/coq/coq/blob/d712096e84579b346bf87341165228c55403dded/user-contrib/Ltac2/Constr.v#L92-L95 It should be possible to add a let-binding to the context and not just a lambda binding cc @coq/ltac2-maintainers

`destruct` is linear in the size of the context and much much slower than `case; clear; intros`

9

#### Description of the problem Consider the code ```coq Fixpoint mkgoal (n : nat) : Prop := match n with | O => True /\ True -> True | S...

#### Description of the problem ```coq Goal True. Proof. ``` gives ``` Error: Anomaly "Stm.join: tip not cached" Please report at http://coq.inria.fr/bugs/. ``` cc @coq/stm-maintainers #### Coq Version https://gitlab.com/coq/coq/-/jobs/2740357137/artifacts/download i.e....

`coqc --config` should not fail when the stdlib cannot be found

12

``` $ coqc --config cannot guess a path for Coq libraries; please use -coqlib option or ensure you have installed the package containing Coq's stdlib (coq-stdlib in OPAM) If you...

[request] Coq selective/filtered import should support blacklists

4

I'd like an equivalent of Agda's `hiding` when doing [filtered import](https://coq.inria.fr/refman/language/core/modules.html#grammar-token-filtered_import), something like `Import foo(-(id, compose))`, which has the effect of adding everything not in the inner parentheses.

#### Description of the problem If `typeclasses eauto with core` is being suggested as a replacement for `eauto`, then it should support `using` as well. cc @mattam82 #### Coq Version...

make install is broken

6

Can it be fixed? ``` /usr/bin/make DESTDIR=//debian/tmp install make[2]: Entering directory '/' To install Coq using dune, use 'dune build -p P && dune install P' where P is any...