Open Hub
Open Hub

 Settings |  Report Duplicate

1
I Use This!
Moderate Activity

Commits : Listings

Analyzed 1 day ago. based on code collected 2 days ago.
Aug 23, 2025 — Aug 23, 2026
Commit Message Contributor Files Modified Lines Added Lines Removed Code Location Date
configure: add "rocq" synonyms for "coq" options
Xavier Leroy
More... 6 days ago
CI golf: run `latest` and `oldest` on PRs; use `latest` Docker image again
Xavier Leroy
More... 7 days ago
Asmgenproof for PowerPC: ensure compatibility with old Coq versions
Xavier Leroy
More... 7 days ago
Update the test suite (again)
Xavier Leroy
More... 7 days ago
Update the test suite
Xavier Leroy
More... 14 days ago
Update documentation on warnings
Xavier Leroy
More... 15 days ago
extraction: use Set Extraction Prefix for compatibility with Rocq 9.4 (#589)
Pierre Roux
More... 15 days ago
Menhirlib: fix misplaced Proof commands
Xavier Leroy
More... 15 days ago
Makefile: use an explicit path for extraction/extraction.v (#591)
Jason Gross
More... 15 days ago
Merge pull request #587 from AbsInt/rocq-9.2
Xavier Leroy
More... about 1 month ago
Notations `#1` and `#2` (for `fst` and `snd`) moved to Coqlib
Xavier Leroy
More... about 1 month ago
String literals in asm files: use asm escapes, not OCaml escapes (#588)
Xavier Leroy
More... about 1 month ago
Asm printing: quote command-line arguments when needed, continued
Xavier Leroy
More... about 2 months ago
Asm printing: quote command-line arguments when needed (#586)
Xavier Leroy
More... about 2 months ago
Merge pull request #585 from AbsInt/no-bitfield-align
Xavier Leroy
More... about 2 months ago
Do not change alignment for packed bit-fields
Bernhard Schommer
More... about 2 months ago
Reject `aligned` attribute on bit fields in struct types
Xavier Leroy
More... about 2 months ago
Update test suite
Xavier Leroy
More... about 2 months ago
Elab: thread environment through `elab_initializer`
Michael Schmidt
More... 2 months ago
Asmgenproof for PowerPC: remove `important_preg`
Xavier Leroy
More... 2 months ago
Add missing `Proof.` commands
Xavier Leroy
More... 2 months ago
x86 / Win64 ABI: fix inconsistency on callee-save XMM registers (#584)
Xavier Leroy
More... 2 months ago
MenhirLib/Interpreter.v: reintroduce `Declare Scope` and re-enable warning
Xavier Leroy
More... 2 months ago
Memory.v: use more portable lemmas from ZArith
Xavier Leroy
More... 2 months ago
Avoid `try (rewrite H; auto)` when `H` may not be an equality
Xavier Leroy
More... 2 months ago
Makefile: update warning options for Rocq 9.2
Xavier Leroy
More... 2 months ago
Put postfix notations at level 1
Xavier Leroy
More... 2 months ago
Rewrite `Proof (term)` as `Proof. exact (term). Qed.`
Xavier Leroy
More... 2 months ago
Explicit declaration of proof hints databases using `Create Hintdb`
Xavier Leroy
More... 2 months ago
GHA CI: update `latest` action to Rocq 9.2.0
Xavier Leroy
More... 3 months ago