MetaCoq/metacoq

Issues

• Please pick the version you prefer for Coq 8.20 in Coq Platform 2025.01

  #1127 opened 2 months ago by MSoegtropIMC
  1

• Anomaly when defining and using inductive types while in interactive proof mode.

  #1129 opened 3 months ago by DeLectionnes
  0

• Improve Quoting to also quote uniform parameters

  #1120 opened 4 months ago by thomas-lamiaux
  2

• Add a tmWarning

  #1119 opened 4 months ago by thomas-lamiaux
  0

• Improve printing functions of `TemplateMonad`

  #1118 opened 4 months ago by MathisBD
  0

• Anomaly as a result of extraction in CertiCoq (assertion fails in ml code)

  #1072 opened 4 months ago by mkarup
  18

• Universe level error when defining dependent types in one metacoq call.

  #1108 opened 5 months ago by DeLectionnes
  4

• `tmMkDefinition` and friends discard the evar map

  #1115 opened 5 months ago by MathisBD
  0

• Using tmMkInductive and tmUnquote unpredictably crashes

  #1114 opened 5 months ago by MathisBD
  0

• `Unquote Definition` will normalize the term

  #1091 opened 9 months ago by WeituoDAI
  0

• Universe inconsistency with MetaCoq and stdpp

  #1090 opened 7 months ago by 4ever2
  4

• Please create a tag for Coq 8.19 in Coq Platform 2024.01

  #1069 opened a year ago by rtetley
  3

• Should default branch be coq-8.18 or main?

  #994 opened a year ago by JasonGross
  4

• Please create a tag for the version of MetaCoq that CertiCoq can depend on

  #1062 opened a year ago by liyishuai
  1

• In 8.18, MetaCoq Run sometimes returns an anomaly when running incorrectly typed code.

  #1042 opened a year ago by DeLectionnes
  1

• [Feature Request] Please allow scripting `#[export] Typeclasses Opaque foo.` in the template monad

  #864 opened 2 years ago by JasonGross
  1

• MetaCoq is missing `Hint Opaque`

  #1004 opened a year ago by Janno
  2

• coq-8.17 branch no longer builds on ocaml 4.11.2

  #1022 opened a year ago by JasonGross
  0

• Please create a tag for Coq 8.18 in Coq Platform 2023.10

  #989 opened a year ago by rtetley
  4

• template-coq/theories/utils/ByteCompareSpec.v is too heavy for coq-native

  #771 opened a year ago by JasonGross
  1

• Please create a tag for Coq 8.17 in Coq Platform 2023.03

  #865 opened 2 years ago by MSoegtropIMC
  7

• [Request] Please add debug support for the template monad

  #878 opened 2 years ago by JasonGross
  0

• [Feature] Please add `tmTry`

  #874 opened 2 years ago by JasonGross
  0

• Please enable auto rebase from the web interface

  #871 opened 2 years ago by JasonGross
  0

• `tmQuoteModule` should return global references in dependency order, without duplicates

  #850 opened 2 years ago by JasonGross
  1

• `tmQuoteModule` incorrectly returns the empty list when a module is bound or aliases a bound module

  #847 opened 2 years ago by JasonGross
  1

• `tmExistingInstance` should support `#[export]` and `#[local]` hints as well

  #840 opened 2 years ago by JasonGross
  0

• Request: `tmLocateModule`

  #852 opened 2 years ago by JasonGross
  0

• Error: Anomaly "Evar ?X40 was not declared." when running template programs with holes which involve `tmDefinition`

  #862 opened 2 years ago by JasonGross
  0

• `tmDefinition` says that MetaCoq tactics are bugged and fail to declare universes

  #853 opened 2 years ago by JasonGross
  2

• `tmUnquote` (or `tmDefinition`) fails to propagate universe constraints

  #842 opened 2 years ago by JasonGross
  2

• Request: `tmOpenModule` and `tmCloseModule`

  #851 opened 2 years ago by JasonGross
  0

• `tmQuoteModule` generates many anomalies

  #846 opened 2 years ago by JasonGross
  0

• Please add `tmFreshUniverse` and `tmUnquoteUniverses`

  #844 opened 2 years ago by JasonGross
  0

• `tmDefinition` should support polymorphic definitions

  #843 opened 2 years ago by JasonGross
  0

• "tm* must take n arguments" errors are incorrect

  #841 opened 2 years ago by JasonGross
  0

• Please add a function for checking if a kername is valid in the global environment, or if it will disappear when the file is finished

  #839 opened 2 years ago by JasonGross
  0

• Please add general fixpoint combinator to the template monad

  #775 opened 2 years ago by JasonGross
  1

• Build fails with "undefined symbol: camlMetacoq_template_plugin__Primitive__7"

  #766 opened 2 years ago by haansn08
  3

• PCUIC should support easy translation from template-polymorphic and universe-polymorphic-with-variance inductives

  #815 opened 2 years ago by JasonGross
  0

• Execution of module initializers in the shared library failed in async mode

  #777 opened 2 years ago by kyoDralliam
  1

• How does one print proof terms as de bruijn indices instead of random named variables in Coq?

  #808 opened 2 years ago by brando90
  2

• missing .glob entries for definitions/inductives created using meta-coq monad

  #794 opened 2 years ago by aa755
  0

• Template program gives Error: Anomaly "in econstr: grounding a non evar-free term" Please report at http://coq.inria.fr/bugs/.

  #779 opened 2 years ago by JasonGross
  0

• metacoq/translations/times_bool_fun2.v is incompatible with the native compiler (Anomaly "Uncaught exception UGraph.UniverseInconsistency(_).")

  #772 opened 2 years ago by JasonGross
  2

• coq-metacoq-translations.dev failing in bench

  #760 opened 2 years ago by SkySkimmer
  3

• 1.1+8.16 does not compile on 32/64 bit Windows

  #764 opened 2 years ago by MSoegtropIMC
  6

• Reasoning about TemplateMonad commands?

  #753 opened 3 years ago by jsarracino
  1

• Question: Nested Function Applications

  #659 opened 3 years ago by justinfargnoli
  2

• Any plans on supporting higher ocaml versions?

  #651 opened 3 years ago by qcfu-bu
  4