Skip to content

Pull requests: MetaRocq/metarocq

New pull request New
34 Open 1,046 Closed
34 Open 1,046 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
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
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
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

Adapt to rocq-prover/rocq#21669 (evaluable_of_global_reference no env arg)
#1242 opened Feb 27, 2026 by SkySkimmer • Draft
[experiment] Use ext-lib monads
#1241 opened Feb 24, 2026 by 4ever2 • Draft
2
doc: Add missing step to include Rocq repo when building from source
#1236 opened Feb 3, 2026 by TDiazT Loading…
Adapt map_term_with_context for 9.1 guard condition
#1234 opened Jan 21, 2026 by BasileGros Loading…
Bump actions/checkout from 4 to 6 dependencies
#1215 opened Nov 21, 2025 by dependabot bot Loading…
Bump actions/checkout from 4 to 6 dependencies
#1214 opened Nov 21, 2025 by dependabot bot Loading…
Bump actions/checkout from 4 to 6 dependencies
#1213 opened Nov 21, 2025 by dependabot bot Loading…
Bump actions/checkout from 4 to 6 dependencies
#1212 opened Nov 21, 2025 by dependabot bot Loading…
Bump actions/checkout from 4 to 6 dependencies
#1211 opened Nov 21, 2025 by dependabot bot Loading…
Bump actions/checkout from 4 to 6 dependencies
#1210 opened Nov 21, 2025 by dependabot bot Loading…
Bump actions/checkout from 4 to 6 dependencies
#1209 opened Nov 20, 2025 by dependabot bot Loading…
Adapt to https://github.com/rocq-prover/stdlib/pull/207
#1204 opened Sep 11, 2025 by proux01 • Draft
Remove eta-expansion in lift_wf_term_it_impl
#1185 opened Jun 19, 2025 by Tragicus Loading…
Correct a broken link to the dependency graph
#1180 opened May 8, 2025 by MevenBertrand Loading…
WIP: implement lazy by lambda in EAst
#1140 opened Jan 29, 2025 by yforster • Draft
Improve evar_map handling in tmMkDefinition and friends
#1111 opened Nov 1, 2024 by MathisBD Loading…
1
Add Nix flakes-based build scripts
#1097 opened Jul 31, 2024 by spacefrogg Loading…
5
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
Add some automation to All_Forall for proving via nth_error
#833 opened Jan 24, 2023 by JasonGross • Draft
2
ProTip! Find all pull requests that aren't related to any open issues with -linked:issue.