ppedrot
Follow
Popular repositories
1,593 contributions in the last year
Less
More
Contribution activity
December 2022
Created 18 commits in 10 repositories
Created a pull request in coq/coq that received 9 comments
Preserve the ESorts abstraction in the upper layers.
We should never go back and forth between the low-level representation and the high level one that keeps a quotient relative to a universe state. O…
+189
−131
•
9
comments
Opened 20 other pull requests in 15 repositories
SkySkimmer/coq-lean-import
1
open
1
merged
LPCIC/coq-elpi
1
open
1
merged
mattam82/Coq-Equations
1
open
1
merged
coq/coq
2
open
MetaCoq/metacoq
2
merged
mit-plv/fiat-crypto
1
merged
lukaszcz/coqhammer
1
open
mit-plv/kami
1
merged
mit-plv/bbv
1
merged
PrincetonUniversity/VST
1
open
ejgallego/coq-serapi
1
merged
jwiegley/category-theory
1
open
coq-community/paramcoq
1
merged
unicoq/unicoq
1
merged
coq-community/aac-tactics
1
merged
Reviewed 10 pull requests in 1 repository
coq/coq
10 pull requests
- Use relevance_of_sort in Typeops.infer_assumption (minicleanup)
- [stub] Introduce sort variables in unification
- Define a dummy replacement for Obj.set_tag for OCaml 5.
- Check VM is enabled in vm_compute
- Separate interpretation and syntax declaration in tactic notations
- Remove the Typeclasses Filtered Unification flag.
- Preserve the ESorts abstraction in the upper layers.
- Remove Flags.native_compiler
- Fix #16922: bug in Nametab.remove which #12324 introduced (deactivation of notations)
- Adapt the bytecode interpreter to the latest changes from OCaml 5.