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
#20262 - Add local qualities to env when Check calls kernel typechecking
Pull Request -
State: open - Opened by SkySkimmer 1 day ago
Labels: kind: fix
#20261 - Error undeclared quality with Check
Issue -
State: open - Opened by SkySkimmer 1 day ago
Labels: kind: bug
#20260 - Print rigid qualities in sorts even if print universes is off
Pull Request -
State: open - Opened by SkySkimmer 1 day ago
Labels: kind: user messages
#20259 - CI: Lean importer repo moved to coq community
Pull Request -
State: closed - Opened by SkySkimmer 1 day ago
- 1 comment
Labels: kind: infrastructure, part: CI
#20258 - Bench add invariant for rocq-runtime
Pull Request -
State: open - Opened by SkySkimmer 1 day ago
- 1 comment
Labels: kind: infrastructure
#20257 - experiment put proofs in main vo segment
Pull Request -
State: open - Opened by SkySkimmer 1 day ago
- 1 comment
Labels: needs: full CI
#20256 - Rocqide try to fix incorrect character conversions
Pull Request -
State: open - Opened by SkySkimmer 1 day ago
- 2 comments
Labels: kind: fix, part: CoqIDE
#20255 - Fix bench false positive detection of failed dependency
Pull Request -
State: closed - Opened by SkySkimmer 2 days ago
- 3 comments
Labels: kind: infrastructure
#20254 - Anomaly "Uncaught exception Not_found." by including a module type in a module
Issue -
State: open - Opened by chatpion 2 days ago
Labels: kind: bug, needs: triage
#20253 - coqdev.el stop using the shim
Pull Request -
State: closed - Opened by SkySkimmer 2 days ago
- 1 comment
Labels: kind: infrastructure
#20252 - Try fixing unification of projections
Pull Request -
State: open - Opened by mattam82 2 days ago
- 4 comments
#20251 - Anomaly "File "pretyping/retyping.ml", line 143, characters 10-16: Assertion failed." with `Set Debug "tactic-unification"`
Issue -
State: open - Opened by Tragicus 2 days ago
- 3 comments
Labels: kind: bug, needs: triage, needs: minimization
#20250 - CI: Fix elpi
Pull Request -
State: closed - Opened by SkySkimmer 2 days ago
- 3 comments
Labels: kind: infrastructure
#20249 - Retype in eta_constructor
Pull Request -
State: open - Opened by Tragicus 2 days ago
- 4 comments
Labels: needs: fixing, needs: full CI
#20248 - check_evar_instance produce nicer error when retyping fails
Pull Request -
State: open - Opened by SkySkimmer 2 days ago
- 3 comments
Labels: kind: user messages
#20247 - `Unset Universe Checking` unifies all sorts
Pull Request -
State: open - Opened by JasonGross 3 days ago
- 3 comments
Labels: kind: fix, part: kernel, part: universes, part: sort polymorphism
#20246 - Unification loop / stack overflow
Issue -
State: open - Opened by EugeneFlesselle 3 days ago
- 2 comments
Labels: kind: bug
#20245 - Ltac2 should support direct manipulation of sorts, universe instances, and constraints
Issue -
State: open - Opened by JasonGross 4 days ago
Labels: part: universes, part: ltac2, kind: wish, part: sort polymorphism
#20244 - Rely on explicit printing of pairs of terms in some module errors
Pull Request -
State: open - Opened by ppedrot 5 days ago
Labels: kind: fix, needs: test-suite update
#20243 - Ltac2.Constr.in_context don't drop goal state
Pull Request -
State: open - Opened by SkySkimmer 5 days ago
- 2 comments
Labels: kind: fix, part: ltac2
#20242 - "Signature components for field ... do not match: expected type ... but found type ..." should never print identical types for the expected and found type
Issue -
State: open - Opened by JasonGross 5 days ago
- 1 comment
Labels: kind: user messages, part: modules, kind: bug, part: sort polymorphism
#20241 - The kernel should permit differing sorts/qualities on sort-polymorphic inductives when `Universe Checking` is unset
Issue -
State: open - Opened by JasonGross 5 days ago
- 4 comments
Labels: kind: bug, part: sort polymorphism
#20240 - Anomaly "Uncaught exception Not_found." when using typeclasses hint mode and failing rewrite/apply due to missing classes.
Issue -
State: open - Opened by Lee-Janggun 6 days ago
Labels: kind: bug, needs: triage
#20239 - ssrmatching cleanups
Pull Request -
State: closed - Opened by SkySkimmer 6 days ago
- 2 comments
Labels: kind: cleanup
#20238 - Update comment in ssreflect.SsrSyntax
Pull Request -
State: closed - Opened by SkySkimmer 6 days ago
- 3 comments
Labels: kind: cleanup, part: ssreflect
#20237 - ci: bump sel to 0.6.0
Pull Request -
State: closed - Opened by gares 6 days ago
- 3 comments
Labels: kind: infrastructure
#20236 - ROCQ_PROFILE_COMPONENTS handle negated list
Pull Request -
State: open - Opened by SkySkimmer 7 days ago
Labels: kind: internal
#20235 - Print/About print arguments with DelimOnlyTmpScope
Pull Request -
State: closed - Opened by SkySkimmer 7 days ago
- 3 comments
Labels: kind: fix, kind: user messages
#20234 - Print/About print binding instances in binder style
Pull Request -
State: open - Opened by SkySkimmer 7 days ago
- 1 comment
Labels: kind: user messages
#20233 - Stop using deprecated typing.io in python code
Pull Request -
State: closed - Opened by SkySkimmer 7 days ago
- 2 comments
Labels: kind: documentation
#20232 - refman-pdf deeper table of contents
Pull Request -
State: open - Opened by SkySkimmer 7 days ago
- 5 comments
Labels: kind: documentation
#20231 - Clarify Set Definitional UIP effect
Pull Request -
State: closed - Opened by SkySkimmer 7 days ago
- 2 comments
Labels: kind: documentation
#20230 - Delay getenv calls
Pull Request -
State: closed - Opened by SkySkimmer 7 days ago
- 5 comments
Labels: kind: fix
#20229 - "Warning, feedback message received but no listener to handle it!"
Issue -
State: closed - Opened by proux01 7 days ago
Labels: kind: user messages, kind: bug
#20228 - Timeout doesn't work
Issue -
State: open - Opened by OwenConoly 8 days ago
- 8 comments
Labels: platform: Windows, kind: bug, needs: triage
#20227 - Evd.is_maybe_typeclass_hook uses econstr
Pull Request -
State: closed - Opened by SkySkimmer 8 days ago
- 1 comment
Labels: kind: cleanup
#20226 - Warning when generating a constraint involving a template universe
Pull Request -
State: open - Opened by SkySkimmer 8 days ago
Labels: kind: user messages, needs: full CI
#20225 - recheck_against don't generate spurious template constraints
Pull Request -
State: open - Opened by SkySkimmer 8 days ago
- 2 comments
Labels: kind: fix
#20224 - `destruct` generates spurious template constraints
Issue -
State: open - Opened by SkySkimmer 8 days ago
Labels: kind: bug
#20223 - Cases do not generate spurious template constraints in `in ...`
Pull Request -
State: open - Opened by SkySkimmer 8 days ago
- 2 comments
Labels: kind: fix
#20222 - Elaboration of `match ... in ...` generates spurious constraints on template inductive
Issue -
State: open - Opened by SkySkimmer 8 days ago
Labels: kind: bug
#20221 - Fix falsely general type variables in Ltac2.List
Pull Request -
State: closed - Opened by SkySkimmer 8 days ago
- 2 comments
Labels: kind: fix
#20220 - Ltac2 Fresh.Free using Nameops.Fresh, add convenience APIs
Pull Request -
State: open - Opened by SkySkimmer 9 days ago
- 1 comment
Labels: kind: enhancement, part: ltac2
#20219 - Add Evd.set_eq_qualities and set_above_prop
Pull Request -
State: closed - Opened by SkySkimmer 9 days ago
- 3 comments
Labels: kind: cleanup
#20218 - Let binder (x:T|P) not depend on the implicit status of sig.
Pull Request -
State: closed - Opened by SkySkimmer 9 days ago
- 1 comment
Labels: kind: enhancement
#20217 - Tac2ffi stop exposing the raw tags
Pull Request -
State: closed - Opened by SkySkimmer 9 days ago
- 7 comments
Labels: kind: cleanup
#20216 - coqc -config should include OCAMLPATH
Issue -
State: open - Opened by JasonGross 10 days ago
- 2 comments
Labels: kind: wish
#20215 - Avoid constructing lists while processing hints
Pull Request -
State: closed - Opened by SkySkimmer 10 days ago
- 17 comments
#20214 - bench export ROCQ_PROFILE_COMPONENTS instead of COQ_...
Pull Request -
State: closed - Opened by SkySkimmer 10 days ago
- 1 comment
Labels: kind: cleanup
#20213 - Fix rocq dep issue with empty string arguments
Pull Request -
State: closed - Opened by Janno 11 days ago
- 6 comments
Labels: kind: fix, part: coqdep
#20212 - coqc hangs on processing a comment & Require Import on Windows, consuming all available memory
Issue -
State: closed - Opened by JasonGross 11 days ago
- 4 comments
Labels: platform: Windows, kind: bug, needs: triage, needs: minimization
#20211 - coqc should error when not given a .v file
Issue -
State: open - Opened by JasonGross 12 days ago
- 4 comments
Labels: kind: user messages, kind: wish
#20210 - eexists and eexists ?[e] behave differently.
Issue -
State: open - Opened by rnrand 12 days ago
Labels: kind: bug, needs: triage
#20209 - `rocq dep` fails on attributes with empty string values in commands that take string arguments
Issue -
State: closed - Opened by Janno 12 days ago
- 2 comments
Labels: kind: regression, kind: bug, part: coqdep
#20208 - coqrst: replace `extra` by `extra-foo` telling what it depends on
Pull Request -
State: closed - Opened by SkySkimmer 12 days ago
- 1 comment
Labels: kind: documentation
#20207 - Ltac2 external check that the name is not already used
Pull Request -
State: closed - Opened by SkySkimmer 12 days ago
- 1 comment
Labels: kind: fix, part: ltac2
#20206 - Ltac2 APIs to manipulate local environments
Pull Request -
State: open - Opened by SkySkimmer 12 days ago
- 4 comments
Labels: kind: feature, part: ltac2
#20205 - `Admitted` should not fail on `Derive` with "Cannot admit: the statement has unresolved existential variables."
Issue -
State: closed - Opened by JasonGross 13 days ago
- 1 comment
Labels: part: derive
#20204 - Do not rely on name canonization in CS cache.
Pull Request -
State: open - Opened by ppedrot 13 days ago
- 7 comments
Labels: kind: cleanup
#20203 - Bench: add coq-elpi to explicit packages
Pull Request -
State: closed - Opened by SkySkimmer 13 days ago
- 3 comments
Labels: kind: infrastructure
#20202 - Add changelog for #19160
Pull Request -
State: closed - Opened by SkySkimmer 13 days ago
Labels: kind: documentation
#20201 - Abstract the datatype of maps of hint modes.
Pull Request -
State: closed - Opened by ppedrot 13 days ago
- 8 comments
Labels: kind: cleanup
#20200 - Description of definitional UIP is ambiguous
Issue -
State: closed - Opened by JasonGross 14 days ago
- 1 comment
Labels: kind: documentation, kind: user messages, kind: wish
#20199 - Non-linear variable pattern in Ltac2 considered an unused variable.
Issue -
State: closed - Opened by jpoiret 14 days ago
- 1 comment
Labels: kind: bug, needs: triage
#20198 - fix bench (coq-bignums -> rocq-bignums)
Pull Request -
State: closed - Opened by SkySkimmer 14 days ago
- 1 comment
Labels: kind: infrastructure
#20197 - Add Ltac2 notation for rename.
Pull Request -
State: open - Opened by jpoiret 14 days ago
Labels: needs: full CI
#20197 - Add Ltac2 notation for rename.
Pull Request -
State: open - Opened by jpoiret 14 days ago
Labels: needs: full CI
#20196 - Collapse environment fields and remove dead API.
Pull Request -
State: closed - Opened by ppedrot 14 days ago
- 1 comment
Labels: kind: cleanup, part: kernel
#20195 - Stop relying on canonicalizing maps in the section mechanism.
Pull Request -
State: closed - Opened by ppedrot 15 days ago
- 1 comment
Labels: kind: cleanup
#20194 - [9.0] [CI] Fix stdlib-doc
Pull Request -
State: closed - Opened by proux01 15 days ago
- 1 comment
Labels: kind: infrastructure
#20193 - Please add the ability to add arbitrary open statements to extracted Ocaml code
Issue -
State: open - Opened by llee454 16 days ago
- 1 comment
Labels: part: extraction, needs: triage, kind: wish
#20192 - Reduce the reliance on CanOrd in upper layers
Pull Request -
State: closed - Opened by ppedrot 16 days ago
- 1 comment
Labels: kind: cleanup
#20191 - Remove automatic adding of coqbin to PATH on windows in envars
Pull Request -
State: open - Opened by SkySkimmer 16 days ago
- 13 comments
Labels: kind: cleanup, platform: Windows
#20190 - Handle queries in rocqshim when possible
Pull Request -
State: closed - Opened by SkySkimmer 16 days ago
- 6 comments
Labels: kind: fix, kind: cleanup, part: build
#20189 - [CI] Fix stdlib-doc
Pull Request -
State: closed - Opened by proux01 16 days ago
- 5 comments
Labels: kind: infrastructure
#20188 - "The variable Notation variable x is not available was not found in the current environment." should be more informative
Issue -
State: open - Opened by JasonGross 17 days ago
- 2 comments
Labels: kind: user messages, part: ltac2, kind: wish
#20187 - Ltac2 format %a should be `'a -> message` not `unit -> 'a -> message`
Issue -
State: open - Opened by JasonGross 17 days ago
- 1 comment
Labels: kind: question, kind: bug, part: ltac2
#20186 - `Ltac2.Control` {throw,assert} functions take formats
Pull Request -
State: open - Opened by JasonGross 17 days ago
- 2 comments
Labels: needs: progress, kind: enhancement, part: ltac2, needs: full CI
#20185 - Request: quality analogue of `max` (or: ability to have primitive projections on more complicated sort-polymorphic records)
Issue -
State: closed - Opened by JasonGross 17 days ago
- 1 comment
Labels: resolved: won't fix, part: primitive records, kind: wish, part: sort polymorphism
#20184 - Add Ltac2.Option.{is_some,is_none,compare,join,iter}
Pull Request -
State: closed - Opened by JasonGross 17 days ago
- 1 comment
Labels: kind: enhancement, part: ltac2
#20183 - Use sets instead of ordered lists in hint stored data.
Pull Request -
State: closed - Opened by ppedrot 17 days ago
- 13 comments
Labels: kind: performance
#20182 - Rename and tweak Modops.add_module_type.
Pull Request -
State: closed - Opened by ppedrot 18 days ago
- 1 comment
Labels: kind: cleanup
#20181 - Set Printing Parentheses does not work as expected
Issue -
State: closed - Opened by eerio 18 days ago
- 2 comments
Labels: kind: bug
#20180 - Issue template: suggest mentioning which interface gets the bug
Pull Request -
State: closed - Opened by SkySkimmer 18 days ago
- 1 comment
Labels: kind: infrastructure
#20179 - Uncaught Exception
Issue -
State: closed - Opened by mukeshtiwari 18 days ago
- 2 comments
Labels: kind: bug, needs: triage
#20178 - Keep qvar in template poly entry and declarations
Pull Request -
State: closed - Opened by SkySkimmer 19 days ago
- 13 comments
Labels: kind: redesign
#20177 - Generate Sort poly eliminator
Pull Request -
State: open - Opened by jpoiret 19 days ago
- 28 comments
#20176 - Stop relying on a global visit state in extraction.
Pull Request -
State: closed - Opened by ppedrot 19 days ago
- 1 comment
Labels: kind: cleanup
#20175 - Support primitive operations in old and new unification.
Pull Request -
State: open - Opened by Janno 19 days ago
- 10 comments
Labels: kind: fix, needs: benchmarking, part: unification, needs: changelog entry, part: primitive types, needs: full CI
#20174 - Fix ci-equations_tests CI script.
Pull Request -
State: closed - Opened by ppedrot 20 days ago
- 3 comments
Labels: kind: infrastructure
#20173 - Fix equations install
Pull Request -
State: closed - Opened by SkySkimmer 20 days ago
- 1 comment
Labels: kind: infrastructure
#20172 - Fix whitespace in rocq usage command
Pull Request -
State: closed - Opened by mattam82 20 days ago
- 3 comments
Labels: kind: fix, kind: user messages
#20171 - Do not add functor delta-resolvers when strengthening.
Pull Request -
State: closed - Opened by ppedrot 20 days ago
- 1 comment
Labels: kind: fix
#20170 - Additional cleanups around the module implementation
Pull Request -
State: closed - Opened by ppedrot 20 days ago
- 3 comments
Labels: kind: cleanup
#20169 - Move timelog2html implementation to rocq-devtools package
Pull Request -
State: closed - Opened by SkySkimmer 20 days ago
- 3 comments
Labels: kind: infrastructure
#20168 - Changes for 9.0, with porting instructions and renaming advice
Pull Request -
State: open - Opened by mattam82 20 days ago
Labels: needs: full CI
#20167 - Remove dead API in Tok.
Pull Request -
State: closed - Opened by ppedrot 20 days ago
- 9 comments
Labels: kind: cleanup
#20166 - [ci] Equations: use dune commands directly
Pull Request -
State: closed - Opened by mattam82 20 days ago
- 3 comments
Labels: kind: infrastructure
#20165 - Export a view type over Environ.env for Serlib and abstract env away.
Pull Request -
State: closed - Opened by ppedrot 20 days ago
- 5 comments
Labels: kind: cleanup
#20164 - Bench explicit package is rocq-equations not coq-equations
Pull Request -
State: closed - Opened by SkySkimmer 20 days ago
- 5 comments
Labels: kind: infrastructure