mattam82/Coq-Equations

Issues

• Warning for inlining Signature for

  #622 opened 2 months ago by thomas-lamiaux
  4

• Deeplim inverses some equalities when sections are involved

  #621 opened 2 months ago by thomas-lamiaux
  1

• Equations taking a long time to type check mutually recursive functions

  #620 opened 2 months ago by JulesViennotFranca
  0

• Anomaly "splitting Equations missing constraints in (anonymous)"

  #597 opened 2 months ago by henriquebg99
  2

• Warnings can't be unset

  #580 opened 2 months ago by YaZko
  1

• Failure to prove functional induction

  #577 opened 2 months ago by terencode
  2

• Anomaly "in Univ.repr: Universe file.v.1700 undefined."

  #614 opened 3 months ago by yiyunliu
  0

• Install/export module with inspect definition and notation like eqn

  #613 opened 5 months ago by palmskog
  0

• Bug with not fully applied term: Anomaly "Uncaught exception Failure("List.chop")"

  #609 opened 6 months ago by thomas-lamiaux
  0

• Limited support when the decreasing argument is a Prop while the return type is in Type

  #598 opened 6 months ago by HuStmpHrrr
  1

• Please pick the version you prefer for Coq 8.19 in Coq Platform 2024.01

  #585 opened 7 months ago by rtetley
  2

• Crash with Coq 8.19

  #583 opened 9 months ago by jjhugues
  0

• Many links broken on http://mattam82.github.io/Coq-Equations/

  #571 opened a year ago by jaccokrijnen
  1

• Generated elimination principle is missing some induction hypotheses

  #576 opened a year ago by RalfJung
  0

• Documentation mentions non-existing symbols

  #575 opened a year ago by RalfJung
  1

• Potential Bug that crashes coqtop

  #572 opened a year ago by Agnishom
  0

• Please pick the version you prefer for Coq 8.18 in Coq Platform 2023.10

  #563 opened a year ago by rtetley
  4

• `List.chop` throws an exception when a recursive call is missing a parameter

  #555 opened a year ago by agrn
  0

• Anomaly "in Univ.repr: Universe Var(0) undefined." with `Derive Signature NoConfusion EqDec for Var.`

  #554 opened a year ago by SkySkimmer
  0

• Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03

  #541 opened 2 years ago by MSoegtropIMC
  1

• Recursive definition is ill-formed

  #542 opened 2 years ago by hflsmax
  1

• Anomaly "in Univ.repr: Universe MetaCoq.SafeChecker.PCUICSafeConversion.12667 undefined." Please report at http://coq.inria.fr/bugs/

  #545 opened 2 years ago by JasonGross
  2

• Subsume funind

  #495 opened 2 years ago by Alizter
  1

• Hang / unlimited memory use with `simp` on trivial function not occurring in Goal

  #538 opened 2 years ago by MSoegtropIMC
  1

• [feature request] Attributes #[transparent/opaque]

  #522 opened 2 years ago by mattam82
  0

• Merely `Require Equations.Prop.Equations.` breaks the derive plugin shipped in Coq's standard library

  #515 opened 2 years ago by JasonGross
  0

• Collisions in case sensitivity cause problems on macOS

  #492 opened 2 years ago by jwiegley
  2

• Stack overflow with UIP

  #498 opened 2 years ago by laMudri
  2

• Notation conflict with standard library

  #505 opened 2 years ago by jwiegley
  1

• Please pick the version you prefer for Coq 8.16 in Coq Platform 2022.09

  #506 opened 2 years ago by MSoegtropIMC
  1

• License: unclear

  #496 opened 2 years ago by SnarkBoojum
  2

• Exception on invalid syntax

  #508 opened 2 years ago by TobiasKappe
  0

• Multiple problems with list

  #500 opened 2 years ago by eponier
  3

• Recursive definitions using wf and returning functions don't work

  #499 opened 2 years ago by lgaeher
  0

• Equations generates wrong variable names

  #493 opened 3 years ago by fkj
  0

• Hang on funelim

  #491 opened 3 years ago by Tuplanolla
  0

• Anomaly when using CoInductive types

  #490 opened 3 years ago by euisuny
  0

• `funelim` with dependently typed function doesn't eliminate

  #488 opened 3 years ago by Lysxia
  0

• Support explicit naming of hypotheses generated by funelim

  #415 opened 3 years ago by anton-trunov
  2

• Equations raises type error where Program generates proof obligation

  #478 opened 3 years ago by elefthei
  0

• Please create a tag for Coq 8.15 in Coq Platform 2022.02

  #471 opened 3 years ago by MSoegtropIMC
  4

• Dangling debug universe level in Equations definitions ?

  #445 opened 3 years ago by kyoDralliam
  2

• Importing Equations 1.3 breaks std++'s 'simplify_eq' tactic

  #449 opened 3 years ago by RalfJung
  1

• Branching on nothing raises an anomaly

  #448 opened 3 years ago by TheoWinterhalter
  0

• In WSL2/ubuntu 21.10: make fails when trying to compile from source

  #447 opened 3 years ago by jibnew
  2

• Failure to derive NoConfusionHom

  #414 opened 3 years ago by co-dan
  1

• Simultaneous definition of terms and notations

  #416 opened 3 years ago by anton-trunov
  1

• Bug: Derive NoConfusion for this inductive seems almost correct, but forgets to apply an argument?

  #441 opened 3 years ago by drcicero
  1

• Unable to install equations: exit with code 4

  #446 opened 3 years ago by Zarickan
  1

• Please create a tag for the upcoming release of Coq 8.14

  #427 opened 3 years ago by MSoegtropIMC
  8