coq

coq copied to clipboard

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

JasonGross

Frequent coq rebuilds due to dune updates

9

#### Description of the problem I am not sure where is the right place to report this, but I feel like there are some pains caused by the dune migration...

RalfJung

[experiment] Separate parsing execution

11

This is an experimental branch, not to be merged directly.

maximedenes

[coqdep] Further cleanup of the loadpath API

5

In particular we remove the `coqlib` field which was just used to suppress a warning. This brings `coqdep/loadpath` closer to `vernac/loadpath.ml`, but still a way to go. Many differences are...

ejgallego

[stdlib] Add properties and predicates on lists with output in Type

45

Add computational content to `List.v`: mainly `Type` is used instead of `Prop` as much as possible. **Kind:** feature. - [ ] Entry added in the changelog

olaure01

[auto] set use_metas_eagerly_in_conv_on_closed_terms = true

13

Setting this flag in `auto` (and `eauto`) makes the resolution be slightly closer to `simple (e)apply`. Also, this behavior is closer to `typeclasses eauto`. Fixes #16323 Fixes #16062 Currently, `debug...

mrhaandi

Avoid lifting for syntactic arities in sort_of_atomic_type

4

Not sure this will have much impact but let's see

SkySkimmer

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

JasonGross

intros. Optimize Proof. takes O(n^3) time

27

#### Version ~~~~~ The Coq Proof Assistant, version 8.8.1 (July 2018) compiled on Jul 5 2018 7:25:50 with OCaml 4.06.0 ~~~~~ #### Operating system Arch Linux, up to date as...

andres-erbsen

Qed diverges at the end of a "Lemma/with" proof

6

Note: the issue was created automatically with bugzilla2github tool Original bug ID: BZ#2727 From: @fpottier Reported version: 8.5 CC: @herbelin, @pirbo

coqbot