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

#19214 - `discriminate` cannot handle sort polymorphic equality

Issue - State: closed - Opened by tabareau 5 months ago - 1 comment
Labels: kind: bug

#19203 - `remember` cannot handle sort-polymorphic registered equality.

Issue - State: closed - Opened by jpoiret 5 months ago - 2 comments
Labels: kind: bug

#19184 - Export side effects of transparent obligations

Pull Request - State: open - Opened by herbelin 5 months ago - 7 comments
Labels: needs: progress, needs: rebase, part: program, kind: enhancement, stale

#19182 - `ltac:( )` quotation no longer supported in `change`

Issue - State: open - Opened by vfukala 5 months ago - 3 comments
Labels: part: ltac, kind: bug

#19177 - [core] Improved state protection against memprof-limits interruptions

Pull Request - State: open - Opened by ejgallego 5 months ago - 54 comments
Labels: kind: fix, needs: testing, part: ocaml, needs: full CI

#19162 - The syntax `Type@{ Set/Prop/SProp | ...}` should be accepted as well by Coq

Issue - State: open - Opened by kyoDralliam 5 months ago - 2 comments
Labels: part: universes, kind: wish, part: gallina

#19132 - [experiment] Reference arities

Pull Request - State: closed - Opened by mattam82 6 months ago - 13 comments
Labels: needs: rebase, stale, needs: full CI

#19117 - Start a GoodDefaults file collecting recommended option settings.

Pull Request - State: closed - Opened by Zimmi48 6 months ago - 20 comments
Labels: needs: progress, kind: feature, needs: rebase, needs: documentation, kind: compatibility, needs: changelog entry, stale, needs: full CI

#19092 - Better integration of Derive in declare.ml + fix of #18951

Pull Request - State: closed - Opened by herbelin 6 months ago - 5 comments
Labels: kind: fix, kind: cleanup, kind: enhancement, part: derive

#19049 - [notations] Warn about incompatible prefixes

Pull Request - State: closed - Opened by proux01 6 months ago - 15 comments
Labels: kind: user messages, part: notations

#19037 - Additions to String module and extraction to OCaml native strings

Pull Request - State: closed - Opened by BridgeTheMasterBuilder 6 months ago - 9 comments
Labels: part: standard library, needs: changelog entry

#19031 - A common execution path for universe restriction + universe declaration check

Pull Request - State: closed - Opened by herbelin 6 months ago - 9 comments
Labels: kind: cleanup, part: universes

#19029 - Experiment the addition of sealed/defined attributes

Pull Request - State: open - Opened by herbelin 6 months ago - 2 comments
Labels: kind: feature, needs: rebase, needs: merge of dependency, part: attributes, part: gallina

#19023 - `abstract:{` tactic block

Pull Request - State: open - Opened by SkySkimmer 6 months ago - 16 comments
Labels: needs: progress, kind: feature

#19007 - [declare] Warn on unused using attributes on sub-obligations

Pull Request - State: closed - Opened by ejgallego 7 months ago - 3 comments
Labels: needs: rebase, stale, needs: full CI

#18971 - ::> only declares an instance without a coercion when it should do both

Issue - State: closed - Opened by Alizter 7 months ago - 2 comments
Labels: kind: bug

#18951 - Anomaly "in Lemmas.save_lemma_admitted: more than one statement." with Derive

Issue - State: closed - Opened by SkySkimmer 7 months ago - 3 comments
Labels: kind: anomaly

#18903 - Algebraic universes and new solving algorithm

Pull Request - State: closed - Opened by mattam82 8 months ago - 44 comments
Labels: needs: rebase, stale

#18900 - Attempt to avoid exporting mono univs from Qed proofs

Pull Request - State: open - Opened by SkySkimmer 8 months ago - 10 comments
Labels: needs: fixing, needs: rebase, needs: full CI

#18882 - Release 8.20

Issue - State: closed - Opened by proux01 8 months ago - 11 comments
Labels: kind: meta

#18869 - Make the usage of Ftactic in Tacinterp more consistent

Pull Request - State: open - Opened by afdw 8 months ago - 5 comments
Labels: needs: rebase, stale, needs: full CI

#18828 - Flag to disable cumulativity of Prop

Pull Request - State: open - Opened by SkySkimmer 8 months ago - 3 comments
Labels: needs: full CI

#18761 - Subtraction in NatInt

Pull Request - State: closed - Opened by Villetaneuse 9 months ago - 6 comments
Labels: kind: cleanup, needs: rebase, part: standard library, kind: enhancement, stale, needs: full CI

#18647 - `Declare ML Module'`s "valid plugin names" restrictions seem to make it impossible to import certain libraries.

Issue - State: open - Opened by tom-p-reichel 9 months ago - 5 comments
Labels: part: build, kind: bug, part: coqdep

#18647 - `Declare ML Module'`s "valid plugin names" restrictions seem to make it impossible to import certain libraries.

Issue - State: open - Opened by tom-p-reichel 9 months ago - 5 comments
Labels: part: build, kind: bug, part: coqdep

#18621 - Take into account the local delta flags for "simpl"

Pull Request - State: open - Opened by herbelin 10 months ago - 7 comments
Labels: needs: fixing, part: tactics, kind: enhancement, part: reduction strategies

#18617 - Fix #18572: tactic clear sometimes too eager to remove a dependency in an existential variable vs restricting the context of the existential variable

Pull Request - State: closed - Opened by herbelin 10 months ago - 39 comments
Labels: needs: fixing, kind: fix, needs: rebase, part: tactics, stale, part: existential variables

#18615 - Declare global sort variables

Pull Request - State: open - Opened by kyoDralliam 10 months ago - 8 comments
Labels: kind: feature, needs: rebase, part: universes, needs: changelog entry, part: vernac, stale

#18581 - Take "simpl never" into account for "simpl" in position of argument of a "match", "fix" or projection

Pull Request - State: closed - Opened by herbelin 10 months ago - 19 comments
Labels: kind: fix, needs: rebase, part: tactics, needs: merge of dependency, part: reduction strategies, stale, needs: full CI

#18575 - Clarify the status of the independence of general premises in file ClassicalFacts.v

Pull Request - State: closed - Opened by herbelin 10 months ago - 4 comments
Labels: part: standard library, kind: enhancement

#18531 - Feature request: universe instances in notations

Issue - State: open - Opened by kyoDralliam 10 months ago - 6 comments
Labels: part: notations, kind: enhancement, kind: wish

#18520 - Qed time is quadratic (sharing of sub-terms is not detected)

Issue - State: open - Opened by fpottier 10 months ago - 41 comments

#18482 - Remove include type

Pull Request - State: closed - Opened by Villetaneuse 10 months ago - 13 comments
Labels: kind: cleanup, needs: rebase, part: modules, stale, needs: full CI

#18385 - [build] Remove the legacy loading mode.

Pull Request - State: closed - Opened by ejgallego 12 months ago - 60 comments
Labels: kind: cleanup, part: build, part: coqdep

#18341 - Fix #18332 (specialize does not support evars in the instantiated args)

Pull Request - State: open - Opened by Matafou 12 months ago - 24 comments
Labels: needs: full CI

#18295 - Doc: move prodn for filtered_import and import_categories

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

#18222 - Failure of "only" selector

Issue - State: closed - Opened by jfehrle about 1 year ago - 2 comments
Labels: part: tactics, part: ltac, resolved: invalid, kind: bug

#18183 - [stdlib] well-founded list extension

Pull Request - State: closed - Opened by mrhaandi about 1 year ago - 10 comments
Labels: part: standard library, kind: enhancement

#18092 - More appropriately moving PropExt->ProofIrrel to file PropExtensionalityFact.v

Pull Request - State: open - Opened by herbelin about 1 year ago - 7 comments
Labels: needs: rebase, part: standard library, stale

#18078 - Idea for a more useful variant of `Hint Mode` `+`

Issue - State: open - Opened by samuelgruetter about 1 year ago - 16 comments
Labels: part: typeclasses, kind: wish

#17945 - Typeclasses feature request: per-Instance mode

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

#17944 - test-suite: Add support for customizing coqchk args

Pull Request - State: open - Opened by JasonGross over 1 year ago
Labels: kind: infrastructure, part: test-suite, needs: full CI

#17943 - CI should display timing info for the test-suite

Issue - State: open - Opened by JasonGross over 1 year ago
Labels: kind: infrastructure

#17942 - Exporting a version of pr_constr_expr/pr_lconstr_expr ensured not to be overriden

Pull Request - State: open - Opened by herbelin over 1 year ago
Labels: kind: cleanup, needs: full CI

#17941 - Command line option '-boot' not documented

Issue - State: open - Opened by jp-diegidio over 1 year ago

#17940 - Briefly rewritten proofs of Finite_sets_facts.v

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

#17939 - math

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

#17938 - Improve the infrastructure of `nia` tests a bit

Pull Request - State: open - Opened by JasonGross over 1 year ago
Labels: kind: infrastructure, part: micromega, part: test-suite

#17937 - Don't specialize dep hyps in zify

Pull Request - State: open - Opened by JasonGross over 1 year ago - 2 comments
Labels: kind: fix, part: micromega

#17936 - `zify` / `Z.euclidean_division_equations_cleanup` should not instantiate dependent hypotheses

Issue - State: open - Opened by JasonGross over 1 year ago
Labels: part: micromega, kind: bug

#17935 - `nia` should be able to prove `x * y = 1 -> x = 1 \/ x = -1`

Issue - State: open - Opened by JasonGross over 1 year ago
Labels: part: micromega

#17934 - Give `Z.to_euclidean_division_equations` more power

Pull Request - State: open - Opened by JasonGross over 1 year ago - 10 comments
Labels: kind: enhancement, needs: benchmarking, part: micromega

#17933 - Add more tests for `nia`

Pull Request - State: open - Opened by JasonGross over 1 year ago - 9 comments
Labels: kind: cleanup, kind: infrastructure, needs: benchmarking, part: micromega, part: test-suite, needs: full CI

#17932 - `hnf` and `simpl` fail to reduce ι-redexes arising from `frshiftexp`

Issue - State: open - Opened by JasonGross over 1 year ago
Labels: kind: bug, part: reduction strategies, part: primitive types

#17931 - Ltac2.Printf.fprintf should support character escapes; Ltac2.Message should be able to print newlines

Issue - State: open - Opened by JasonGross over 1 year ago
Labels: kind: user messages, kind: enhancement, part: ltac2

#17930 - Fix build after concurrent merge of #17875 and #17827

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

#17929 - Constant_typing: eliminating the detour via type "result"

Pull Request - State: open - Opened by herbelin over 1 year ago - 1 comment
Labels: kind: cleanup

#17928 - Don't use boolean in interp_search_restriction, and expose it

Pull Request - State: open - Opened by SkySkimmer over 1 year ago
Labels: needs: overlay, kind: internal

#17927 - add Z.divide support for Z.to_euclidean_division_equations

Pull Request - State: open - Opened by doctor-kaliy over 1 year ago - 2 comments
Labels: part: standard library, kind: enhancement, part: micromega, needs: full CI

#17926 - Pass bound universes directly as an instance in the VM.

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

#17925 - Variant of `#[export] Set` which is reverted at the end of `Import`

Issue - State: open - Opened by JasonGross over 1 year ago - 2 comments
Labels: part: modules, kind: enhancement, part: attributes, kind: wish

#17923 - coqide-server package runs tests which require coq to be built

Issue - State: open - Opened by gares over 1 year ago - 1 comment
Labels: part: build

#17922 - Add attribution for `Acc_intro_generator`.

Pull Request - State: open - Opened by robbertkrebbers over 1 year ago - 3 comments

#17921 - [release] script to publish opam packages

Pull Request - State: open - Opened by gares over 1 year ago
Labels: kind: infrastructure, kind: meta, needs: full CI

#17920 - ssrbool: reenable overwriting-delimiting-key

Pull Request - State: open - Opened by JasonGross over 1 year ago - 3 comments
Labels: kind: user messages, part: ssreflect, kind: enhancement

#17919 - [release] bump version to 8.18+rc1

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

#17918 - `Z.to_euclidean_division_equations` should support `Z.divide`

Issue - State: open - Opened by JasonGross over 1 year ago - 1 comment
Labels: part: standard library, good first issue

#17916 - [release] V8.18 backports

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

#17915 - Remove geocoq from CI

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 7 comments
Labels: kind: infrastructure, kind: ci-failure

#17914 - faster setoid_ring/Ncring_polynom.v

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

#17913 - Advertise Ltac2 in Ltac chapter.

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

#17911 - exposing interp_search_restriction

Pull Request - State: open - Opened by ThomasPortet over 1 year ago - 4 comments
Labels: kind: internal

#17910 - Weird typing anomaly with setoid rewrite on dependent types

Issue - State: open - Opened by ppedrot over 1 year ago - 1 comment
Labels: kind: anomaly, part: unification, part: rewriting tactics

#17909 - Produce warning+dynamic error on missing notation variable in Ltac2

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

#17907 - For arguments scopes, statically know the list of available scopes (technical PR)

Pull Request - State: closed - Opened by herbelin over 1 year ago - 1 comment
Labels: kind: cleanup, part: sections

#17903 - Fixes #10878: let Number Notation be insensitive to the implicit arguments of its parameters

Pull Request - State: closed - Opened by herbelin over 1 year ago - 7 comments
Labels: part: notations, kind: enhancement

#17902 - Fixes #11237: support constructor with parameters in primitive notations for patterns

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

#17899 - Add a file to spot-check the specs of primitive floats

Pull Request - State: open - Opened by JasonGross over 1 year ago - 6 comments
Labels: kind: infrastructure, part: test-suite, part: primitive types, needs: full CI

#17895 - Porting coq-plugin-lib from coq 8.9 to coq 8.10

Issue - State: open - Opened by agrarpan over 1 year ago - 8 comments

#17891 - Fixes #17782: anomaly when trying to disable a non existing custom notation

Pull Request - State: closed - Opened by herbelin over 1 year ago - 6 comments
Labels: kind: fix, part: notations

#17888 - Discharge on the fly

Pull Request - State: open - Opened by herbelin over 1 year ago - 44 comments
Labels: kind: feature, part: kernel, needs: full CI

#17883 - [experiment] Delayed substitution in VM normalization of telescopes.

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

#17878 - Declaration of Ltac2 primitives using a GADT-based mechanism

Pull Request - State: open - Opened by rlepigre over 1 year ago - 3 comments
Labels: needs: documentation, needs: full CI

#17875 - Add printer support for grammar entries with non-necessary-lower level on their right-hand side

Pull Request - State: closed - Opened by herbelin over 1 year ago - 4 comments
Labels: kind: fix, part: notations, part: printer

#17869 - Ltac2 imprecise typechecking errors in match branches

Issue - State: open - Opened by samuelgruetter over 1 year ago - 4 comments

#17866 - Fix broken link in XML protocol documentation.

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

#17864 - Tuning native_compute optimizations?

Issue - State: closed - Opened by JasonGross over 1 year ago - 2 comments
Labels: part: native compiler, kind: question, kind: wish

#17856 - Notation wish #17845: add support for notations with recursive binders involving "let" and "match"

Pull Request - State: open - Opened by herbelin over 1 year ago - 1 comment
Labels: part: notations, kind: enhancement, needs: full CI

#17840 - [coqidetop] Fix print depth setting for Richpp clients

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

#17839 - Add primitives for controlling reduction

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

#17838 - Make TC observers summary safe

Pull Request - State: open - Opened by SkySkimmer over 1 year ago
Labels: needs: test-suite update, kind: internal

#17835 - coq_makefile: make .filestoinstall during the rule needing it

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

#17832 - Reformulating the grammar of rewstrategy with GRAMMAR EXTEND

Pull Request - State: open - Opened by herbelin over 1 year ago - 6 comments
Labels: kind: fix, part: parser, part: printer, part: rewriting tactics, needs: full CI

#17827 - Notations: collecting the notation variables binding in a given notation variable

Pull Request - State: closed - Opened by herbelin over 1 year ago - 11 comments
Labels: part: notations, kind: internal

#17818 - Move typed_vernac to its own file from vernacextend

Pull Request - State: open - Opened by SkySkimmer over 1 year ago - 2 comments
Labels: kind: cleanup, part: vernac, request: full CI, needs: full CI

#17813 - `ListNotations` breaks primitive array syntax

Issue - State: open - Opened by JasonGross over 1 year ago - 5 comments
Labels: part: standard library, part: notations, part: primitive types

#17807 - Make TC resolution hook Summary safe

Issue - State: open - Opened by ejgallego over 1 year ago
Labels: priority: blocker