Labels · coq/coq

part: standard library

The standard library stdlib.

79

part: STM

State Transition Machine, asynchronous proofs, etc.

72

part: tactics

328

part: test-suite

The testing suite.

20

part: tools

Coqdoc, coq_makefile, etc.

39

part: toplevel

11

part: typeclasses

The typeclass mechanism.

83

part: unification

The unification mechanism.

75

part: universes

The universe system.

96

part: vernac

High level command interpretation.

45

part: VM

Virtual machine.

24

part: website

Submit website issues at https://github.com/coq/www

3

part: xml protocol

4

platform: macOS

This is a macOS specific issue.

13

platform: Nix

This is a Nix specific issue.

1

platform: Windows

This is a Windows specific issue.

32

priority: blocker

The next release should be delayed if this is not fixed.

priority: high

The priority for inclusion in the next release is high.

8

request: full CI

Use this label when you want your next push to trigger a full CI.

resolved: answered

Question was answered.

resolved: duplicate(d)

Closed in favor of another issue about the same bug.

resolved: fixed in newer version

By the time the issue was reported, it was already fixed. To be completed by a milestone when known.

resolved: invalid

Not an actual bug.

resolved: moved

Moved to another bug / issue tracker.

resolved: won't fix

There are no plans to fix this.

1

resolved: works for me

Cannot reproduce the problem.

reverted

This pull request was finally reverted.

stale

This PR will be closed unless it is rebased.

5

wellknown: ltac variable bypasses typechecking

typically `let x := constr:(y) in clear y; use x`

10

wellknown: the int clash extraction problem

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

No labels!

153 labels