Skip to content

Issues: MetaRocq/metarocq

Beta
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

Clear current search query, filters, and sorts
63 Open 96 Closed
63 Open 96 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
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Explicit sharing enhancement question
#343 opened Nov 16, 2019 by gmalecha
Bug in test-suite/TypingTests.v
#19 opened Feb 10, 2018 by SimonBoulier
Defining lambda from Ast
#24 opened Mar 28, 2018 by hfehrmann
1
Variant types
#71 opened Sep 26, 2018 by vzaliva
Constr vs Econstr
#82 opened Jan 9, 2019 by SimonBoulier
1
PCUIC vs Ast.term
#108 opened Mar 27, 2019 by gmalecha
28
extraction mode: adding level to environment in unquote_universe bug
#119 opened Apr 9, 2019 by aa755
3
Port translations to the Extractable TemplateMonad
#130 opened Apr 29, 2019 by gmalecha
8
Compatibility with HoTT
#139 opened May 20, 2019 by annenkov
5
Verified extraction to OCaml
#163 opened Jun 6, 2019 by palmskog
8
Helper function for tCase
#237 opened Jul 20, 2019 by Lysxia
5
Enable tmDefinition to generate local definitions
#305 opened Sep 26, 2019 by gmalecha
Universes are slow
#13 opened Feb 3, 2018 by mattam82
avoid duplication when quoting records with primitive projections
#326 opened Oct 24, 2019 by tabareau
Primitive projections are not registered when defining a record
#369 opened Jan 31, 2020 by kyoDralliam
1
Unrestricted Recursion (tmFix) in TemplateMonad
#377 opened Feb 13, 2020 by fakusb
4
Examples of generating universe polymorphic code?
#396 opened Apr 6, 2020 by gmalecha
1
Recursive TemplateMonad programs are slow to run
#441 opened Jul 16, 2020 by john-ml
1
2
Quoting and denoting of universes is not an inverse
#449 opened Aug 1, 2020 by gmalecha
3
Unquoting constant with wrong modpath raises anomaly
#452 opened Aug 3, 2020 by yforster
3
Add compile time dependency on python to readme
#463 opened Sep 12, 2020 by DKuhse
1
Cleaning headers
#478 opened Sep 22, 2020 by SimonBoulier
2
make all does not build translations, but make install does
#489 opened Sep 28, 2020 by yforster
Unquoting polymorphic inductives is broken
#512 opened Nov 10, 2020 by annenkov
4
λ-box pretty-printer giving incorrect names in mutual fixpoint
#1182 opened May 19, 2025 by simon-dima
1
ProTip! Type g i on any issue or pull request to go back to the issue listing page.