coq/coq issues and pull requests | Ecosyste.ms: Issues

#11416 - Include all relevant paths in call to ocamldebug (dune)

Pull Request - State: closed - Opened by MSoegtropIMC about 5 years ago - 1 comment
Labels: needs: progress, kind: infrastructure

#11237 - String notation and pattern matching: “No interpretation for string [...]”

Issue - State: closed - Opened by lthms about 5 years ago - 6 comments
Labels: part: notations

#11151 - vm reduction is sometimes quadratic in the number of binders

Issue - State: open - Opened by JasonGross over 5 years ago - 21 comments
Labels: kind: performance

#11071 - [Feature Request] Set Debug {Cbn,Simpl,Lazy} like Set Debug Cbv

Issue - State: open - Opened by JasonGross over 5 years ago - 4 comments
Labels: kind: feature, kind: user messages, kind: enhancement

#11066 - Automatically generate bidirectional hints

Issue - State: open - Opened by SkySkimmer over 5 years ago - 4 comments
Labels: kind: wish, kind: design discussion, part: records

#10846 - Add python script to gather CI failure statistics from gitlab

Pull Request - State: closed - Opened by MSoegtropIMC over 5 years ago - 22 comments
Labels: needs: progress, kind: infrastructure

#10821 - FR: build coq using dune without coqide dependencies

Issue - State: closed - Opened by andres-erbsen over 5 years ago - 9 comments
Labels: part: build, kind: wish

#10741 - Combination of `lia` and `lra`

Issue - State: open - Opened by maximedenes over 5 years ago - 9 comments
Labels: kind: feature, part: micromega

#10741 - Combination of `lia` and `lra`

Issue - State: open - Opened by maximedenes over 5 years ago - 8 comments
Labels: kind: feature, part: micromega

#10613 - Suggestion to install internal binaries to /usr/lib or /usr/libexec

Issue - State: closed - Opened by aaronpuchert over 5 years ago - 9 comments
Labels: help wanted, part: installation, part: build

#10370 - [Ltac2] : Add system functions for writing and reading files and running processes

Pull Request - State: closed - Opened by MSoegtropIMC over 5 years ago - 6 comments

#10290 - CoqIDE 8.10beta1 preference menu hangs several seconds before loading

Issue - State: closed - Opened by charguer over 5 years ago - 13 comments
Labels: kind: performance, part: CoqIDE, needs: triage

#10207 - Partly revert micromega parsing using typeclasses.

Pull Request - State: closed - Opened by fajb almost 6 years ago
Labels: kind: fix, part: micromega

#10167 - do not parse `|` as infix in patterns; parse `|}` as `|` `}`

Pull Request - State: closed - Opened by ggonthier almost 6 years ago - 45 comments
Labels: kind: cleanup, part: notations

#10167 - do not parse `|` as infix in patterns; parse `|}` as `|` `}`

Pull Request - State: closed - Opened by ggonthier almost 6 years ago - 45 comments
Labels: kind: cleanup, part: notations

#10166 - Partly revert micromega parsing using typeclasses.

Pull Request - State: closed - Opened by fajb almost 6 years ago - 5 comments
Labels: kind: fix, part: micromega

#10136 - [ltac2] Add primitive integers

Pull Request - State: closed - Opened by proux01 almost 6 years ago
Labels: kind: enhancement, part: ltac2

#9856 - A 'zify' tactic as a ML plugin

Pull Request - State: closed - Opened by fajb almost 6 years ago - 54 comments
Labels: kind: feature, kind: performance

#9803 - Adding more trigonometry in Reals

Pull Request - State: closed - Opened by thery almost 6 years ago - 96 comments
Labels: kind: feature, part: standard library

#9803 - Adding more trigonometry in Reals

Pull Request - State: closed - Opened by thery almost 6 years ago - 96 comments
Labels: kind: feature, part: standard library

#9717 - The documentation of `+` and `tclOR` both tell lies

Issue - State: open - Opened by JasonGross almost 6 years ago - 13 comments
Labels: kind: documentation, part: ltac

#9285 - Feature Request: Set Debug Rewrite

Issue - State: open - Opened by JasonGross about 6 years ago - 1 comment
Labels: kind: performance, part: tactics, kind: enhancement, part: rewriting tactics

#9199 - Dune build: don't require a bash for building

Issue - State: open - Opened by MSoegtropIMC about 6 years ago - 23 comments
Labels: kind: feature, kind: infrastructure, platform: Windows, part: build

#9083 - Import BinInt massively slows down printing by 400x without changing the printed expression

Issue - State: open - Opened by JasonGross about 6 years ago - 4 comments
Labels: kind: performance, kind: user messages, part: notations

#8853 - [feature request] String syntax notations should live in user-land, not plugin land

Issue - State: closed - Opened by JasonGross over 6 years ago - 5 comments
Labels: kind: feature, part: notations, kind: enhancement

#8853 - [feature request] String syntax notations should live in user-land, not plugin land

Issue - State: closed - Opened by JasonGross over 6 years ago - 5 comments
Labels: kind: feature, part: notations, kind: enhancement

#8512 - Fix issue #8511 merge-pr.sh does not check if user.email and user.sig…

Pull Request - State: closed - Opened by MSoegtropIMC over 6 years ago - 15 comments
Labels: needs: progress, needs: rebase, kind: infrastructure

#8356 - String: add reverse function

Pull Request - State: closed - Opened by liyishuai over 6 years ago - 31 comments
Labels: kind: feature, needs: discussion, part: standard library, needs: overlay

#8092 - Request for option to disable use of the native_compute cache

Issue - State: open - Opened by JasonGross over 6 years ago - 6 comments
Labels: part: native compiler, kind: enhancement

#7959 - Recursive notation with "pairs" as recursive pattern

Issue - State: open - Opened by anton-trunov over 6 years ago - 16 comments
Labels: part: notations

#7913 - Defining mutually recursive fixpoints as (definitional) type class instances

Issue - State: closed - Opened by ifazk over 6 years ago - 7 comments
Labels: part: typeclasses, kind: enhancement, kind: design discussion, part: inductives

#7847 - Test-suite should enable native compilation

Issue - State: open - Opened by ppedrot over 6 years ago - 8 comments
Labels: kind: infrastructure, part: test-suite, needs: triage

#7711 - Stdlib 2 meta issue

Issue - State: closed - Opened by maximedenes over 6 years ago - 6 comments
Labels: kind: redesign, part: standard library, kind: design discussion

#7710 - limiting (typeclass) hint usage

Issue - State: open - Opened by andres-erbsen over 6 years ago - 3 comments
Labels: part: modules, part: typeclasses

#7424 - Inductive type sort annotations are ignored

Issue - State: closed - Opened by andres-erbsen almost 7 years ago - 3 comments
Labels: part: universes

#7362 - nested proofs cause uncaught exception

Issue - State: closed - Opened by andrew-appel almost 7 years ago - 1 comment
Labels: resolved: won't fix, kind: anomaly

#7267 - Define a function using tactics without a type

Issue - State: open - Opened by nomeata almost 7 years ago - 9 comments
Labels: kind: enhancement

#6757 - Various issues with Prop thought or not as as member of the Type hierarchy

Issue - State: closed - Opened by herbelin about 7 years ago
Labels: part: universes

#6724 - What commit from 3rd party developments should CI test?

Issue - State: closed - Opened by SkySkimmer about 7 years ago - 61 comments
Labels: kind: infrastructure, food for thought, part: CI

#6245 - Would there be a way to have an overview of where an intervention from us is needed?

Issue - State: closed - Opened by herbelin about 7 years ago - 1 comment
Labels: kind: meta

#6127 - [feature request] "dynamic" scopes in notations

Issue - State: open - Opened by JasonGross over 7 years ago - 2 comments
Labels: part: notations, kind: enhancement

#6012 - eq_true vs is_true

Issue - State: closed - Opened by herbelin over 7 years ago - 4 comments
Labels: needs: feedback, part: standard library, kind: question

#5997 - The error message "has type "Type@{Top.4}" which should be coercible to "Type@{Coq.Init.Datatypes.23}"." is wrong

Issue - State: closed - Opened by JasonGross over 7 years ago - 1 comment
Labels: kind: user messages, part: kernel

#5657 - Confusing universe inconsistency report which in Coq 8.5 first reports as strict positivity issue

Issue - State: closed - Opened by coqbot over 7 years ago - 3 comments
Labels: part: kernel, resolved: invalid

#5605 - There should be a [Set Ltac Debug Under Typeclasses] option

Issue - State: open - Opened by coqbot over 7 years ago - 3 comments
Labels: part: ltac

#5563 - test-suite/all_stdlib.v not properly made from installed Coq

Issue - State: closed - Opened by coqbot over 7 years ago - 1 comment
Labels: part: tools

#5458 - Apply and "Ill-typed evar instance"

Issue - State: open - Opened by coqbot almost 8 years ago - 5 comments
Labels: part: tactics, part: unification

#5436 - [Print Ltac] should print all implicit arguments that show up in patterns

Issue - State: open - Opened by coqbot almost 8 years ago - 1 comment
Labels: kind: user messages, part: ltac

#5342 - Case analysis on sort Set is not allowed error message could be more helpful

Issue - State: open - Opened by coqbot about 8 years ago - 1 comment
Labels: kind: user messages, good first issue

#5330 - Warn about not using "Proof." -- and maybe other fixable reasons for synchronous processing

Issue - State: closed - Opened by coqbot about 8 years ago - 3 comments
Labels: kind: user messages

#5327 - Feature request: a variant of cbv that lifts let-binders above application without unnecessarily inlining them

Issue - State: closed - Opened by coqbot about 8 years ago - 2 comments
Labels: part: tactics, resolved: duplicate(d)

#5282 - Error: Unexpected error during scheme creation: Error: x is used in conclusion.

Issue - State: open - Opened by coqbot about 8 years ago - 4 comments
Labels: part: tactics

#5279 - Bogus "Error: Unable to decide equality of type arguments."

Issue - State: closed - Opened by coqbot about 8 years ago - 3 comments
Labels: part: tactics

#5271 - Modular white lists for cbv

Issue - State: open - Opened by coqbot about 8 years ago - 4 comments
Labels: part: tactics

#5236 - Suggestion about transitivity/etransitivity

Issue - State: open - Opened by coqbot about 8 years ago - 2 comments
Labels: kind: feature, part: tactics

#5224 - Warning: Invalid character (Windows 10)

Issue - State: closed - Opened by coqbot about 8 years ago - 2 comments
Labels: platform: Windows

#5195 - LtacProf: structured feedback gives bogus total_time

Issue - State: closed - Opened by coqbot over 8 years ago - 2 comments
Labels: part: ltac, platform: Windows

#5167 - simpl ignores some reduction hints

Issue - State: open - Opened by coqbot over 8 years ago - 1 comment
Labels: part: tactics

#5115 - enahncement: find all instances of a typeclass, regardless of args, without solving arg subgoals

Issue - State: open - Opened by coqbot over 8 years ago - 8 comments
Labels: part: ltac

#5105 - Cannot infer this placeholder

Issue - State: closed - Opened by coqbot over 8 years ago - 2 comments
Labels: part: tactics

#4917 - Anomaly: Uncaught exception Invalid_argument("run_com"). Please report.

Issue - State: closed - Opened by coqbot over 8 years ago - 2 comments
Labels: part: ltac

#4808 - Anomaly: File "proofs/proofview_monad.ml", line 43, characters 12-18: Assertion failed. Please report.

Issue - State: closed - Opened by coqbot over 8 years ago - 6 comments
Labels: part: tactics, kind: anomaly

#4790 - Feature request: a way to specify -native-code on a per-file (or per-definition, or per-term) basis

Issue - State: open - Opened by coqbot over 8 years ago - 2 comments
Labels: part: native compiler, kind: enhancement

#4613 - "Time -" does not behave like "-"

Issue - State: open - Opened by coqbot almost 9 years ago - 1 comment
Labels: part: tactics

#4583 - [Implicit Type] declarations not honored while pretty printing

Issue - State: closed - Opened by coqbot about 9 years ago - 2 comments
Labels: part: notations, kind: enhancement

#4175 - "Error: build_signature: no constraint can apply on a dependent argument" should not be fatal (It is possible to break [rewrite_strat] by adding hints that don't break [autorewrite])

Issue - State: open - Opened by coqbot almost 10 years ago - 7 comments
Labels: part: tactics, part: rewriting tactics

#4022 - Autorewrite does less than it used to

Issue - State: closed - Opened by coqbot about 10 years ago - 3 comments
Labels: part: tactics, resolved: won't fix

#4003 - Application of argument module functors inside of module types is too weak; it should enforce equality of bodies, and not just types

Issue - State: open - Opened by coqbot about 10 years ago - 26 comments
Labels: part: modules

GitHub / coq/coq issues and pull requests