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

#19830 - CI: add elpi as dependency for CoRN

Pull Request - State: open - Opened by MSoegtropIMC 4 days ago - 5 comments
Labels: needs: full CI

#19829 - [ci] Remove SerAPI from CI.

Pull Request - State: closed - Opened by ejgallego 5 days ago - 4 comments
Labels: kind: infrastructure, part: CI

#19828 - Fix missing attribution in changelog for #18385

Pull Request - State: closed - Opened by SkySkimmer 5 days ago - 1 comment
Labels: kind: documentation, kind: internal

#19827 - Declare ML Module allow plugin names not containing `.`

Pull Request - State: open - Opened by SkySkimmer 5 days ago - 3 comments
Labels: kind: fix, part: build, part: coqdep

#19827 - Declare ML Module allow plugin names not containing `.`

Pull Request - State: open - Opened by SkySkimmer 5 days ago - 3 comments
Labels: kind: fix, part: build, part: coqdep

#19826 - Coqinit split init_runtime to better support having multiple docs

Pull Request - State: open - Opened by SkySkimmer 5 days ago - 1 comment
Labels: kind: internal

#19825 - 8.20 backports

Pull Request - State: closed - Opened by proux01 5 days ago
Labels: needs: full CI

#19825 - 8.20 backports

Pull Request - State: closed - Opened by proux01 5 days ago
Labels: needs: full CI

#19824 - Provide a way to associate a name with a `Hint Extern`

Pull Request - State: open - Opened by jfehrle 8 days ago
Labels: needs: full CI

#19823 - Show "autoapply" tactic for tc eauto debug; include dbnames in tactic for info where needed

Pull Request - State: open - Opened by jfehrle 8 days ago - 1 comment
Labels: part: tactics, needs: full CI

#19823 - Show "autoapply" tactic for tc eauto debug; include dbnames in tactic for info where needed

Pull Request - State: open - Opened by jfehrle 8 days ago - 1 comment
Labels: part: tactics, needs: full CI

#19822 - rm problematic variables under lambdas and evars for evar instantiation

Pull Request - State: open - Opened by Tragicus 8 days ago - 28 comments
Labels: needs: test-suite update, needs: full CI

#19821 - `tc eauto` fails to backtrack on evar assignment

Issue - State: closed - Opened by jfehrle 9 days ago - 2 comments
Labels: part: tactics, kind: bug, needs: triage

#19821 - `tc eauto` fails to backtrack on evar assignment

Issue - State: closed - Opened by jfehrle 9 days ago - 2 comments
Labels: part: tactics, kind: bug, needs: triage

#19820 - Remove "stdlib2" from CI

Pull Request - State: open - Opened by SkySkimmer 9 days ago

#19820 - Remove "stdlib2" from CI

Pull Request - State: open - Opened by SkySkimmer 9 days ago

#19819 - CClosure don't mk_clos on fletin type

Pull Request - State: closed - Opened by SkySkimmer 9 days ago - 2 comments

#19819 - CClosure don't mk_clos on fletin type

Pull Request - State: closed - Opened by SkySkimmer 9 days ago - 2 comments

#19818 - Use warning attribute

Pull Request - State: closed - Opened by proux01 9 days ago
Labels: kind: cleanup, part: ssreflect

#19818 - Use warning attribute

Pull Request - State: closed - Opened by proux01 9 days ago
Labels: kind: cleanup, part: ssreflect

#19817 - Remove `dfs eauto`, deprecated in 8.16

Pull Request - State: closed - Opened by jfehrle 10 days ago - 2 comments
Labels: kind: cleanup

#19817 - Remove `dfs eauto`, deprecated in 8.16

Pull Request - State: closed - Opened by jfehrle 10 days ago - 2 comments
Labels: kind: cleanup

#19816 - Provide a way to give a name on Hint Extern (affects Hint Cut and Remove Hints)

Issue - State: open - Opened by jfehrle 10 days ago
Labels: kind: question, needs: triage, kind: wish

#19816 - Provide a way to give a name on Hint Extern (affects Hint Cut and Remove Hints)

Issue - State: open - Opened by jfehrle 10 days ago
Labels: kind: question, needs: triage, kind: wish

#19815 - coqdep and dune_rule_gen fixes before removal of legacy loading

Pull Request - State: closed - Opened by SkySkimmer 10 days ago - 2 comments
Labels: kind: fix, part: build

#19814 - Debug print for `lazy` (wip)

Pull Request - State: open - Opened by SkySkimmer 10 days ago - 17 comments
Labels: needs: full CI

#19813 - Windows CI update upload-artifact version

Pull Request - State: closed - Opened by SkySkimmer 10 days ago - 4 comments
Labels: kind: infrastructure

#19813 - Windows CI update upload-artifact version

Pull Request - State: closed - Opened by SkySkimmer 10 days ago - 4 comments
Labels: kind: infrastructure

#19812 - Update CODE_OF_CONDUCT.md

Pull Request - State: open - Opened by tabareau 11 days ago
Labels: needs: full CI

#19812 - Update CODE_OF_CONDUCT.md

Pull Request - State: open - Opened by tabareau 11 days ago
Labels: needs: full CI

#19811 - Better primitive projections handling in tactics and pretyper.

Pull Request - State: open - Opened by jpoiret 11 days ago
Labels: needs: full CI

#19811 - Better primitive projections handling in tactics and pretyper.

Pull Request - State: open - Opened by jpoiret 11 days ago
Labels: needs: full CI

#19810 - removed uses and of Zeq_bool in setoid_ring

Pull Request - State: open - Opened by ybertot 11 days ago - 2 comments

#19810 - removed uses and of Zeq_bool in setoid_ring

Pull Request - State: open - Opened by ybertot 11 days ago - 2 comments

#19809 - Reduce most artifacts expire_in to 1 week

Pull Request - State: closed - Opened by SkySkimmer 12 days ago - 3 comments
Labels: kind: infrastructure

#19809 - Reduce most artifacts expire_in to 1 week

Pull Request - State: closed - Opened by SkySkimmer 12 days ago - 3 comments
Labels: kind: infrastructure

#19808 - Create HintDb does not erase pre-existing hint db

Pull Request - State: open - Opened by SkySkimmer 12 days ago - 1 comment

#19807 - Apparently missing “if” in plugins/extraction/scheme.ml

Pull Request - State: closed - Opened by forked-from-1kasper 12 days ago - 5 comments
Labels: kind: fix

#19807 - Apparently missing “if” in plugins/extraction/scheme.ml

Pull Request - State: closed - Opened by forked-from-1kasper 12 days ago - 5 comments
Labels: kind: fix

#19806 - Constant Extraction doesn't work with Scheme

Issue - State: closed - Opened by Borschemancer 12 days ago
Labels: kind: bug, needs: triage

#19806 - Constant Extraction doesn't work with Scheme

Issue - State: closed - Opened by Borschemancer 12 days ago
Labels: kind: bug, needs: triage

#19805 - Use the release Dune profile when running `configure` during opam package installation

Pull Request - State: open - Opened by dra27 13 days ago - 5 comments
Labels: kind: fix, part: build, needs: full CI

#19804 - 8.20 backports

Pull Request - State: closed - Opened by proux01 13 days ago
Labels: needs: full CI

#19803 - Remove the meta state from evarmaps

Pull Request - State: open - Opened by ppedrot 14 days ago - 18 comments
Labels: kind: cleanup

#19803 - Remove the meta state from evarmaps

Pull Request - State: open - Opened by ppedrot 14 days ago - 18 comments
Labels: kind: cleanup

#19802 - Doc: Add an explicit example where let x := u in v is well-typed while (fun x => v) u is not

Pull Request - State: closed - Opened by jeanas 15 days ago - 1 comment
Labels: kind: documentation

#19802 - Doc: Add an explicit example where let x := u in v is well-typed while (fun x => v) u is not

Pull Request - State: closed - Opened by jeanas 15 days ago - 1 comment
Labels: kind: documentation

#19801 - make Zeq_bool an alias for Z.eqb, deprecate ZArith_Base

Pull Request - State: open - Opened by andres-erbsen 15 days ago - 25 comments
Labels: kind: cleanup, part: standard library, needs: changelog entry, needs: full CI

#19801 - make Zeq_bool an alias for Z.eqb, deprecate ZArith_Base

Pull Request - State: open - Opened by andres-erbsen 15 days ago - 25 comments
Labels: kind: cleanup, part: standard library, needs: changelog entry, needs: full CI

#19800 - ZMicromega does not depend on Q

Pull Request - State: open - Opened by andres-erbsen 15 days ago - 2 comments
Labels: kind: cleanup, part: standard library, part: micromega

#19800 - ZMicromega does not depend on Q

Pull Request - State: open - Opened by andres-erbsen 15 days ago - 2 comments
Labels: kind: cleanup, part: standard library, part: micromega

#19799 - `debug auto` output does not include all lemmas used during the proof

Issue - State: open - Opened by andres-erbsen 15 days ago - 2 comments
Labels: kind: user messages, kind: bug, needs: triage, part: auto

#19799 - `debug auto` output does not include all lemmas used during the proof

Issue - State: open - Opened by andres-erbsen 15 days ago - 2 comments
Labels: kind: user messages, kind: bug, needs: triage, part: auto

#19798 - RFC: Split stdlib Program into Init and deprecated

Pull Request - State: open - Opened by andres-erbsen 17 days ago - 3 comments
Labels: kind: cleanup, part: standard library, part: program, needs: merge of dependency

#19798 - RFC: Split stdlib Program into Init and deprecated

Pull Request - State: open - Opened by andres-erbsen 17 days ago - 3 comments
Labels: kind: cleanup, part: standard library, part: program, needs: merge of dependency

#19797 - use Program less in stdlib

Pull Request - State: open - Opened by andres-erbsen 17 days ago - 7 comments
Labels: kind: cleanup, part: standard library, part: program, needs: overlay

#19797 - use Program less in stdlib

Pull Request - State: open - Opened by andres-erbsen 17 days ago - 7 comments
Labels: kind: cleanup, part: standard library, part: program, needs: overlay

#19796 - RFC: ZMicromega and ZArithRing without ZArith_base

Pull Request - State: open - Opened by andres-erbsen 17 days ago - 2 comments
Labels: kind: cleanup, part: standard library, needs: merge of dependency

#19796 - RFC: ZMicromega and ZArithRing without ZArith_base

Pull Request - State: open - Opened by andres-erbsen 17 days ago - 2 comments
Labels: kind: cleanup, part: standard library, needs: merge of dependency

#19795 - add_field: pass pre/post arguments down to add_ring

Pull Request - State: open - Opened by gares 17 days ago - 15 comments
Labels: kind: fix, needs: full CI

#19795 - add_field: pass pre/post arguments down to add_ring

Pull Request - State: open - Opened by gares 17 days ago - 15 comments
Labels: kind: fix, needs: full CI

#19794 - Reduce the dependency on metas in several parts of the code

Pull Request - State: closed - Opened by ppedrot 18 days ago - 9 comments
Labels: kind: cleanup

#19794 - Reduce the dependency on metas in several parts of the code

Pull Request - State: closed - Opened by ppedrot 18 days ago - 9 comments
Labels: kind: cleanup

#19793 - Documentation: "dependent destruction" uses extra axioms

Issue - State: open - Opened by jeanas 18 days ago - 1 comment
Labels: kind: documentation

#19793 - Documentation: "dependent destruction" uses extra axioms

Issue - State: open - Opened by jeanas 18 days ago - 1 comment
Labels: kind: documentation

#19792 - ZMicromega only uses BinInt not ZArith_base; deprecate Ztac

Pull Request - State: open - Opened by andres-erbsen 18 days ago - 8 comments
Labels: kind: cleanup, part: standard library

#19792 - ZMicromega only uses BinInt not ZArith_base; deprecate Ztac

Pull Request - State: open - Opened by andres-erbsen 18 days ago - 8 comments
Labels: kind: cleanup, part: standard library

#19791 - Simplify proof of Peano_dec.le_unique

Pull Request - State: open - Opened by jeanas 18 days ago - 3 comments
Labels: kind: cleanup, part: standard library, needs: full CI

#19791 - Simplify proof of Peano_dec.le_unique

Pull Request - State: open - Opened by jeanas 18 days ago - 3 comments
Labels: kind: cleanup, part: standard library, needs: full CI

#19790 - Transparent has no effect on a module sealed constant (and no warning/error); About doesn't show the constant's status

Issue - State: open - Opened by jfehrle 18 days ago
Labels: kind: bug, needs: triage, part: gallina

#19789 - split Zdivisibility from Znumtheory, deprecate most of Znumtheory

Pull Request - State: open - Opened by andres-erbsen 19 days ago - 6 comments
Labels: kind: cleanup, part: standard library, needs: changelog entry

#19789 - split Zdivisibility from Znumtheory, deprecate most of Znumtheory

Pull Request - State: open - Opened by andres-erbsen 19 days ago - 6 comments
Labels: kind: cleanup, part: standard library, needs: changelog entry

#19788 - Use correct tactics in TC eauto output; show "Resolve thm" in Print HintDb rather than "simple apply thm", which is not always what's used

Issue - State: open - Opened by jfehrle 19 days ago - 4 comments
Labels: needs: triage, kind: wish

#19788 - Use correct tactics in TC eauto output; show "Resolve thm" in Print HintDb rather than "simple apply thm", which is not always what's used

Issue - State: open - Opened by jfehrle 19 days ago - 4 comments
Labels: needs: triage, kind: wish

GitHub / coq/coq issues and pull requests