Skip to content

Pull requests: MetaCoq/metacoq

New pull request New
22 Open 913 Closed
22 Open 913 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Milestones
Filter by milestone
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

Bump cachix/install-nix-action from 25 to 27
dependencies
#1082 opened May 15, 2024 by dependabot bot Loading…
faster PCUICSR
#1081 opened May 8, 2024 by mrhaandi Loading…
3
Remove useless calls to Eval vm_compute.
#1079 opened Apr 12, 2024 by silene Loading…
Take relevance into account for typing
#1075 opened Apr 5, 2024 by yannl35133 Loading…
Add StateT Monad Transformer
#952 opened Apr 20, 2023 by JasonGross Loading…
6
Add PCUICAstUtils.decompose_app_cps
#951 opened Apr 20, 2023 by JasonGross Loading…
Only run nix on push events and if the word is in the commit message
#950 opened Apr 20, 2023 by yforster Loading…
1
Optimize tmBind
#916 opened Apr 8, 2023 by JasonGross • Draft
1
1
Move some general utility lemmas from TypingWf to All_Forall
#913 opened Apr 8, 2023 by JasonGross • Draft
Make All universe polymorphic
#888 opened Apr 2, 2023 by JasonGross • Draft
1
Add a kludgy implementation of tmTry
#876 opened Mar 28, 2023 by JasonGross Loading…
1
Adapt to coq/coq#16967 (increased kerpair checking)
#875 opened Mar 28, 2023 by SkySkimmer • Draft
Add some automation to All_Forall for proving via nth_error
#833 opened Jan 24, 2023 by JasonGross • Draft
2
Run make to update template-coq/gen-src/cRelationClasses.mli.orig
#791 opened Nov 22, 2022 by JasonGross • Draft
8
Define a minimal subset of Module(Type) Declarations in template-coq
#739 opened Jul 13, 2022 by SwampertX • Draft
SProp
#708 opened May 20, 2022 by yannl35133 • Draft
Universes clause check
#704 opened May 10, 2022 by mattam82 • Draft
PCUIC PHOAS
#573 opened Jul 12, 2021 by mattam82 Loading…
1
Definition of weak-head-reduction and proof of unicity of derivations
#543 opened Feb 16, 2021 by mattam82 • Draft
QuickChick
#173 opened Jun 14, 2019 by mattam82 • Draft
Compute Dependencies in the extractable monad
#133 opened May 8, 2019 by gmalecha • Draft
8
[WIP] [Broken] Fixing parametricity for fixpoint
#94 opened Feb 18, 2019 by CohenCyril Loading…
5
ProTip! no:milestone will show everything without a milestone.