Skip to content

Issues: MetaCoq/metacoq

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.

Sign up for GitHub

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

59 Open 93 Closed
59 Open 93 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

tmMkDefinition and friends discard the evar map
#1115 opened Nov 4, 2024 by MathisBD
Using tmMkInductive and tmUnquote unpredictably crashes
#1114 opened Nov 4, 2024 by MathisBD
Universe level error when defining dependent types in one metacoq call.
#1108 opened Oct 25, 2024 by DeLectionnes
4
Unquote Definition will normalize the term
#1091 opened Jun 24, 2024 by WeituoDAI
Anomaly as a result of extraction in CertiCoq (assertion fails in ml code)
#1072 opened Apr 1, 2024 by mkarup
16
coq-8.17 branch no longer builds on ocaml 4.11.2
#1022 opened Nov 30, 2023 by JasonGross
MetaCoq is missing Hint Opaque
#1004 opened Nov 2, 2023 by Janno
2
Should default branch be coq-8.18 or main?
#994 opened Oct 16, 2023 by JasonGross
4
[Feature] Please add tmTry
#874 opened Mar 26, 2023 by JasonGross
Please enable auto rebase from the web interface
#871 opened Mar 22, 2023 by JasonGross
[Feature Request] Please allow scripting #[export] Typeclasses Opaque foo. in the template monad
#864 opened Mar 1, 2023 by JasonGross
1
Error: Anomaly "Evar ?X40 was not declared." when running template programs with holes which involve tmDefinition
#862 opened Feb 28, 2023 by JasonGross
tmDefinition says that MetaCoq tactics are bugged and fail to declare universes
#853 opened Feb 21, 2023 by JasonGross
2
Request: tmOpenModule and tmCloseModule
#851 opened Feb 21, 2023 by JasonGross
tmQuoteModule generates many anomalies
#846 opened Feb 14, 2023 by JasonGross
Please add tmFreshUniverse and tmUnquoteUniverses
#844 opened Feb 14, 2023 by JasonGross
tmDefinition should support polymorphic definitions
#843 opened Feb 14, 2023 by JasonGross
tmUnquote (or tmDefinition) fails to propagate universe constraints
#842 opened Feb 14, 2023 by JasonGross
2
"tm* must take n arguments" errors are incorrect
#841 opened Feb 14, 2023 by JasonGross
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 Feb 12, 2023 by JasonGross
PCUIC should support easy translation from template-polymorphic and universe-polymorphic-with-variance inductives
#815 opened Dec 14, 2022 by JasonGross
How does one print proof terms as de bruijn indices instead of random named variables in Coq?
#808 opened Dec 11, 2022 by brando90
2
missing .glob entries for definitions/inductives created using meta-coq monad
#794 opened Dec 1, 2022 by aa755
Template program gives Error: Anomaly "in econstr: grounding a non evar-free term" Please report at http://coq.inria.fr/bugs/.
#779 opened Oct 28, 2022 by JasonGross
metacoq/translations/times_bool_fun2.v is incompatible with the native compiler (Anomaly "Uncaught exception UGraph.UniverseInconsistency(_).")
#772 opened Oct 13, 2022 by JasonGross
2
ProTip! Mix and match filters to narrow down what you’re looking for.