Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / coq/coq issues and pull requests

#17561 - 'eauto using' fails on (some) primitive projections

Issue - State: open - Opened by RalfJung over 1 year ago

#17560 - Add `reg` theorems for `nat` on multiplication

Pull Request - State: open - Opened by HaoYang670 over 1 year ago - 14 comments
Labels: needs: full CI

#17559 - Bench: generate html timing tables with links to the html files

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 8 comments
Labels: kind: infrastructure

#17558 - Tweak CList.firstn: return original list when fully used

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 9 comments
Labels: kind: performance

#17556 - Ltac2 should internally distinguish between int and boolean

Issue - State: closed - Opened by jfehrle over 1 year ago - 4 comments
Labels: kind: question, part: ltac2

#17552 - tclFOCUSID: when used on a shelved goal, shelve all produced goals

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 2 comments
Labels: kind: fix, part: tactics

#17550 - Make detyping of projections parameter recovery more robust

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 2 comments
Labels: kind: fix

#17549 - Add test for #16715

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 1 comment
Labels: kind: infrastructure

#17548 - Stop calling inductive indices "annotations" in the doc

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 4 comments
Labels: kind: cleanup, kind: documentation

#17547 - UState.union does not merge sort qualities correctly

Issue - State: closed - Opened by SkySkimmer over 1 year ago

#17546 - Move DefAttributes and with_section_locality back to vernacentries

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 1 comment
Labels: kind: cleanup, kind: internal, part: attributes, part: vernac

#17545 - Use meta_instance instead of an adhoc function in clenv_unique_resolver.

Pull Request - State: closed - Opened by ppedrot over 1 year ago - 4 comments
Labels: kind: cleanup

#17544 - Attribute #[clearbody] useful instead of Let ... Qed

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 21 comments
Labels: kind: redesign, kind: cleanup, kind: compatibility, part: sections, part: attributes, part: vernac, kind: design discussion, kind: usability

#17542 - Merge tests using misc/coqdoc-options

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 1 comment
Labels: kind: fix, kind: infrastructure

#17541 - Stop reducing case analyses when the head is a constructor in case_pf.

Pull Request - State: closed - Opened by ppedrot over 1 year ago - 9 comments
Labels: kind: fix

#17540 - Add CMap.ExtS.symmetric_diff

Pull Request - State: open - Opened by LasseBlaauwbroek over 1 year ago - 19 comments
Labels: needs: full CI

#17534 - Ltac2: use 0 argument externals when possible

Pull Request - State: open - Opened by SkySkimmer over 1 year ago
Labels: needs: discussion, needs: overlay, needs: full CI

#17533 - Ltac2: Make it possible to define externals with other plugin names

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 3 comments
Labels: kind: fix

#17532 - [refman] Add link to the deprecation policy

Pull Request - State: closed - Opened by proux01 over 1 year ago - 6 comments
Labels: kind: documentation

#17531 - Incorrect glob with abbreviation in pattern

Issue - State: closed - Opened by SkySkimmer over 1 year ago - 1 comment

#17524 - Ltac2 unsafe_constr scope

Issue - State: open - Opened by JasonGross over 1 year ago - 1 comment
Labels: kind: feature, kind: wish

#17521 - Ltac2 Compile

Pull Request - State: open - Opened by SkySkimmer over 1 year ago - 8 comments
Labels: kind: feature, kind: performance, part: ltac2, needs: full CI

#17515 - A big update pass on the contributing guide.

Pull Request - State: closed - Opened by Zimmi48 over 1 year ago - 6 comments
Labels: kind: documentation, kind: meta

#17509 - rewrite strategies: expose fixpoint operator

Pull Request - State: open - Opened by SkySkimmer over 1 year ago - 3 comments
Labels: needs: changelog entry, needs: test-suite update, needs: full CI

#17507 - Support multiple :name:s with multiple signatures for .. tacn::

Pull Request - State: open - Opened by jfehrle over 1 year ago - 13 comments
Labels: needs: fixing, kind: documentation, needs: full CI

#17506 - CoqIDE cuts off menus in MacOS

Issue - State: open - Opened by andrew-appel over 1 year ago
Labels: part: IDE, kind: bug

#17505 - Turn "algebraic on the right" error into regular univ inconsistency

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 6 comments
Labels: kind: user messages

#17503 - Add head reduction flags (`lazy head beta` etc)

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 20 comments
Labels: needs: discussion, needs: rebase, stale

#17502 - Correct typo in changes for #15668

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago
Labels: kind: documentation

#17497 - Renaming: update env instead of postprocessing

Pull Request - State: open - Opened by SkySkimmer over 1 year ago - 21 comments
Labels: needs: progress

#17483 - coqdep: Option `-w` to adjust warnings

Pull Request - State: closed - Opened by swasey over 1 year ago - 5 comments
Labels: needs: fixing, needs: rebase, kind: user messages, kind: enhancement, part: coqdep, stale, needs: full CI

#17482 - Ltac2 precomputed values

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 1 comment
Labels: kind: feature, needs: documentation, needs: changelog entry, part: ltac2, needs: full CI

#17479 - Declaremods: do not protect summaries

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 7 comments
Labels: kind: cleanup

#17475 - Ltac2: allow 0 argument externals

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 18 comments
Labels: kind: enhancement, part: ltac2

#17468 - Ltac2: add primitives to build and compare Ltac2.Init.cast

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 4 comments
Labels: kind: enhancement, part: ltac2

#17467 - Validate Proof command: runs typing.ml on the current proof

Pull Request - State: open - Opened by SkySkimmer over 1 year ago - 11 comments
Labels: kind: enhancement

#17466 - typing.ml checks relevance annotations

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 59 comments
Labels: kind: fix

#17422 - More robust reinterpreting of ltac variables

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 9 comments
Labels: kind: fix

#17421 - CoqIDE UI improvements and fixes

Pull Request - State: open - Opened by Frigory33 over 1 year ago - 20 comments
Labels: needs: full CI

#17404 - How to get source code locations for Ltac2 debugger?

Pull Request - State: closed - Opened by jfehrle over 1 year ago
Labels: needs: rebase, kind: question, part: ltac2, needs: full CI

#17394 - [vernac] Remove LoadPath edition vernacular commands

Pull Request - State: open - Opened by ejgallego over 1 year ago - 1 comment

#17393 - [library] Allow require to load libraries from memory.

Pull Request - State: open - Opened by ejgallego over 1 year ago - 4 comments
Labels: needs: rebase, kind: enhancement, needs: overlay, kind: internal, part: vernac, stale

#17388 - API to delay registering the printer for a warning

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 1 comment
Labels: needs: full CI

#17385 - Fix documentation after change of default locality in #16258.

Pull Request - State: open - Opened by Zimmi48 over 1 year ago
Labels: kind: documentation, priority: blocker, needs: full CI

#17382 - [xml protocol] [coqide] Alternative PR fixing some loc problems in master.

Pull Request - State: open - Opened by ejgallego over 1 year ago - 50 comments
Labels: kind: fix, part: CoqIDE, kind: enhancement, priority: blocker, part: xml protocol

#17377 - Build stdlib with per line timings + bench stdlib with -j1

Pull Request - State: open - Opened by SkySkimmer over 1 year ago - 10 comments
Labels: needs: rebase, kind: infrastructure, needs: full CI

#17375 - [stdlib] enumerate permutations

Pull Request - State: open - Opened by haansn08 over 1 year ago - 4 comments
Labels: needs: rebase, part: standard library, kind: enhancement, needs: full CI

#17368 - Bench: add per line info for major and minor word gc stats

Pull Request - State: open - Opened by SkySkimmer over 1 year ago - 16 comments
Labels: needs: progress, needs: rebase, kind: infrastructure, needs: test-suite update

#17365 - [ci] Add coq-http

Pull Request - State: closed - Opened by liyishuai over 1 year ago - 49 comments
Labels: kind: infrastructure, part: CI

#17359 - Ltac2 preterm antiquotation `$$x`

Pull Request - State: open - Opened by SkySkimmer over 1 year ago - 3 comments
Labels: kind: enhancement

#17347 - Ltac2: Add set and map APIs for ident string int constant inductive constructor

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 16 comments
Labels: kind: feature, part: ltac2

#17346 - Ltac1 and Ltac2: don't normalize evars for constr:() and open_constr:()

Pull Request - State: open - Opened by SkySkimmer over 1 year ago - 68 comments
Labels: needs: progress, kind: performance

#17344 - Fixes #10739: anomaly with Extraction within a module

Pull Request - State: open - Opened by herbelin over 1 year ago - 4 comments
Labels: kind: fix, needs: rebase, part: extraction

#17341 - Extraction: extend pruning of unused declarations after inlining to modules

Pull Request - State: open - Opened by herbelin over 1 year ago - 3 comments
Labels: kind: fix, part: extraction, needs: full CI

#17340 - Inline identity projections in extraction

Pull Request - State: open - Opened by herbelin over 1 year ago - 3 comments
Labels: part: extraction, needs: merge of dependency, needs: full CI

#17339 - Fix use of dot notation for non-primitive projections in functors for OCaml extraction

Pull Request - State: closed - Opened by herbelin over 1 year ago - 3 comments
Labels: kind: fix, needs: rebase, part: extraction, needs: merge of dependency, stale

#17336 - coqpp generates invalid line directives

Issue - State: closed - Opened by ejgallego over 1 year ago
Labels: part: tools, kind: bug

#17330 - Scoped infix notation for Ltac2 operators

Issue - State: open - Opened by JasonGross over 1 year ago - 3 comments
Labels: part: ltac2, kind: wish

#17324 - Fixing shadowing of record fields in extraction to OCaml

Pull Request - State: closed - Opened by herbelin over 1 year ago - 4 comments
Labels: part: extraction, kind: bug

#17302 - Support extraction of template-polymorphism types in Prop by means of coercions

Pull Request - State: open - Opened by herbelin over 1 year ago - 2 comments
Labels: kind: fix, part: extraction, kind: enhancement, needs: full CI

#17266 - Experiment: command modifier and tactic for allocation limits

Pull Request - State: open - Opened by SkySkimmer over 1 year ago - 9 comments
Labels: needs: rebase, needs: full CI

#17258 - move ZModulo to test suite

Pull Request - State: open - Opened by andres-erbsen almost 2 years ago - 13 comments
Labels: kind: cleanup, needs: full CI

#17223 - Elpi/HB job out of memory in hulk.v

Issue - State: closed - Opened by SkySkimmer almost 2 years ago - 7 comments

#17207 - Non deterministic coqc output

Issue - State: open - Opened by SkySkimmer almost 2 years ago - 6 comments
Labels: Coq Consortium support services

#17202 - Adding "assumption id" to tell explicitly which assumption to use

Pull Request - State: closed - Opened by herbelin almost 2 years ago - 17 comments
Labels: part: tactics, kind: enhancement, needs: full CI

#17196 - `rewrite lem by tac` in `rewrite_strat`

Issue - State: open - Opened by QinshiWang almost 2 years ago - 1 comment

#17130 - remove Zdigits

Pull Request - State: closed - Opened by andres-erbsen almost 2 years ago - 6 comments
Labels: needs: rebase, stale, needs: full CI

#17123 - Support for string constant tokens in notations

Pull Request - State: closed - Opened by herbelin almost 2 years ago - 6 comments
Labels: needs: rebase, part: notations, kind: enhancement, stale, needs: full CI

#17120 - Backports to v8.17

Pull Request - State: open - Opened by Zimmi48 almost 2 years ago - 1 comment

#17071 - Anomaly "Uncaught exception Failure("List.skipn")."

Issue - State: closed - Opened by afdw almost 2 years ago - 3 comments
Labels: kind: anomaly

#17048 - Fix tooltips

Pull Request - State: open - Opened by jfehrle almost 2 years ago - 2 comments
Labels: part: IDE, needs: full CI

#17043 - [RFC WIP] define modular arithmetic in theories/Numbers/Zmod.v

Pull Request - State: closed - Opened by andres-erbsen almost 2 years ago - 14 comments
Labels: needs: rebase, part: standard library, stale, needs: full CI

#16979 - LtacProf makes tactics very slow

Issue - State: open - Opened by andres-erbsen almost 2 years ago - 7 comments
Labels: kind: performance

#16977 - [DO NOT MERGE] Dummy PR for testing coqbot ci minimize

Pull Request - State: open - Opened by JasonGross almost 2 years ago - 34 comments
Labels: needs: rebase, stale

#16967 - Check correctness of kerpairs in kernel

Pull Request - State: open - Opened by SkySkimmer almost 2 years ago - 76 comments
Labels: needs: fixing, needs: full CI

#16890 - Handle deprecation attribute for definition-like constructions

Pull Request - State: closed - Opened by maximedenes almost 2 years ago - 14 comments
Labels: kind: user messages, kind: enhancement

#16886 - Do not use global variables in Vmbytegen.

Pull Request - State: open - Opened by ppedrot almost 2 years ago - 10 comments
Labels: kind: cleanup, kind: performance

#16861 - CoqIDE: fix save preferences in case GTK user preferences base folder…

Pull Request - State: closed - Opened by MSoegtropIMC almost 2 years ago - 2 comments
Labels: kind: fix, part: CoqIDE, platform: macOS

#16855 - Rename nonterminals in mlgs to be consistent with those used in documentation

Pull Request - State: open - Opened by jfehrle almost 2 years ago - 25 comments
Labels: kind: cleanup, needs: rebase, kind: documentation, stale

#16819 - Allow monomorphic side effects for polymorphic opaques

Pull Request - State: closed - Opened by SkySkimmer about 2 years ago - 5 comments
Labels: needs: discussion

#16813 - Ltac2 types and constructors not properly included

Issue - State: open - Opened by rlepigre about 2 years ago - 5 comments
Labels: part: modules, kind: bug, part: ltac2

#16807 - `coqc -time` prints `<genarg:identref>` for `Derive`

Issue - State: open - Opened by JasonGross about 2 years ago - 5 comments
Labels: kind: user messages, good first issue

#16790 - CoqIDE crashes on long .v files on Mac (M1)

Issue - State: open - Opened by ianshil about 2 years ago - 7 comments
Labels: part: IDE, platform: macOS

#16767 - [nametab] Introduce type of imperative nametabs, unify API

Pull Request - State: open - Opened by ejgallego about 2 years ago - 10 comments
Labels: needs: rebase, stale, needs: full CI

#16716 - Ltac2 should never elide top-level arguments of uncaught exceptions (constr failed to print)

Issue - State: closed - Opened by JasonGross about 2 years ago - 3 comments
Labels: kind: user messages, part: ltac2

#16546 - Fine-grained tactic backtraces

Issue - State: open - Opened by JasonGross about 2 years ago - 4 comments
Labels: kind: user messages, part: ltac, part: ltac2, kind: wish, kind: usability

#16534 - Anomaly "Evar ?X3577 was not declared. on `transparent_abstract`(?)

Issue - State: closed - Opened by JasonGross about 2 years ago - 4 comments
Labels: kind: anomaly

#16484 - [libobject] Common metadata for declared objects

Pull Request - State: open - Opened by ejgallego about 2 years ago - 12 comments
Labels: kind: redesign, kind: feature, needs: rebase, needs: full CI

#16412 - `constr:(ltac:(let v := tac in refine v))` should not be almost 2x slower than `tac`

Issue - State: closed - Opened by JasonGross about 2 years ago - 14 comments
Labels: kind: performance, part: ltac, part: ltac2

#16394 - Allow Ltac2 notations from within Ltac1

Pull Request - State: open - Opened by ppedrot about 2 years ago - 19 comments
Labels: kind: feature, part: ltac2, needs: full CI

#16366 - [vernac] Proof mode without STM

Pull Request - State: open - Opened by gares over 2 years ago - 33 comments
Labels: kind: cleanup, needs: rebase, kind: internal, part: vernac, part: parser, stale, needs: full CI

#16261 - [libobject] Store definition location in the .vo files

Pull Request - State: open - Opened by ejgallego over 2 years ago - 43 comments
Labels: kind: feature, needs: rebase, part: IDE, kind: enhancement, needs: merge of dependency, part: search, needs: full CI

#16190 - Simple compiler for benchmark

Pull Request - State: open - Opened by ejgallego over 2 years ago - 71 comments
Labels: needs: full CI

#16093 - Add coq-http to CI

Issue - State: closed - Opened by Alizter over 2 years ago - 1 comment
Labels: kind: infrastructure

#16079 - [coqdep] Turn dependency resolution failure from a warning to a fatal error

Pull Request - State: open - Opened by ejgallego over 2 years ago - 43 comments
Labels: kind: fix, needs: rebase, needs: independent fix, kind: infrastructure, needs: changelog entry, part: build, part: coqdep, needs: full CI

#15936 - Package uint63.ml and friends separately

Issue - State: open - Opened by ana-borges over 2 years ago - 11 comments
Labels: part: primitive types

#15758 - CI: reenable Coq Platform based Windows CI

Pull Request - State: closed - Opened by MSoegtropIMC over 2 years ago - 4 comments
Labels: kind: infrastructure, platform: Windows, part: CI

#15661 - Fixes #5698: let simpl grants the never flag for primitive projections independently of the internal unfolded status

Pull Request - State: open - Opened by herbelin almost 3 years ago - 17 comments
Labels: needs: progress, kind: fix, kind: cleanup, part: primitive records, part: reduction strategies, needs: full CI

#15637 - Ltac2: complete Int functions with div, mod, abs and logical functions

Pull Request - State: closed - Opened by MSoegtropIMC almost 3 years ago - 1 comment
Labels: kind: enhancement, part: ltac2