-
Notifications
You must be signed in to change notification settings - Fork 43
Issues: mattam82/Coq-Equations
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Author
Label
Projects
Milestones
Assignee
Sort
Issues list
Install/export module with inspect definition and notation like eqn
#613
opened Jul 11, 2024 by
palmskog
Bug with not fully applied term: Anomaly "Uncaught exception Failure("List.chop")"
#609
opened Jun 11, 2024 by
thomas-lamiaux
Limited support when the decreasing argument is a Prop while the return type is in Type
#598
opened May 16, 2024 by
HuStmpHrrr
Anomaly "splitting Equations missing constraints in (anonymous)"
#597
opened May 14, 2024 by
henriquebg99
Generated elimination principle is missing some induction hypotheses
#576
opened Dec 22, 2023 by
RalfJung
Many links broken on http://mattam82.github.io/Coq-Equations/
#571
opened Nov 14, 2023 by
jaccokrijnen
List.chop
throws an exception when a recursive call is missing a parameter
#555
opened Jul 25, 2023 by
agrn
Anomaly "in Univ.repr: Universe Var(0) undefined." with
Derive Signature NoConfusion EqDec for Var.
#554
opened Jul 10, 2023 by
SkySkimmer
Hang / unlimited memory use with
simp
on trivial function not occurring in Goal
#538
opened Feb 14, 2023 by
MSoegtropIMC
Merely
Require Equations.Prop.Equations.
breaks the derive plugin shipped in Coq's standard library
#515
opened Oct 25, 2022 by
JasonGross
Previous Next
ProTip!
Exclude everything labeled
bug
with -label:bug.