index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2020-03-25
Merge PR #11785: [proof] consolidation of mutual definition declaration path
Gaëtan Gilbert
2020-03-25
Merge PR #11875: Fix deploy of refman following #11855.
Gaëtan Gilbert
2020-03-25
Update changelog
Pierre Roux
2020-03-25
Nicer printing for decimal constants in Q
Pierre Roux
2020-03-25
Nicer printing for decimal constants in R
Pierre Roux
2020-03-25
Add a specific opam file to build te docker image
Pierre Roux
2020-03-25
[declare] make restrict_ucontext an optional parameter.
Emilio Jesus Gallego Arias
2020-03-25
[lemmas] Use direct-style for mutual lemma declaration.
Emilio Jesus Gallego Arias
2020-03-25
[lemmas] Use direct-style for variable declaration.
Emilio Jesus Gallego Arias
2020-03-25
[proof] [mutual] Factorize mutual per-entry information
Emilio Jesus Gallego Arias
2020-03-25
[proof] [mutual] Factorize universe handling.
Emilio Jesus Gallego Arias
2020-03-25
[proof] [mutual] Factorize mutual body construction.
Emilio Jesus Gallego Arias
2020-03-25
[proof] [mutual] Factorize notation declaration.
Emilio Jesus Gallego Arias
2020-03-25
[proof] Factorize call info message in mutual declarations
Emilio Jesus Gallego Arias
2020-03-25
[proof] Start of mutual definition save refactoring.
Emilio Jesus Gallego Arias
2020-03-24
Merge PR #11703: Making of NumTok an API for numeral
Pierre-Marie Pédrot
2020-03-24
Merge PR #11772: [obligations] Don't allocate libobjects for obligation info.
Pierre-Marie Pédrot
2020-03-24
Merge PR #11826: [proof] Deprecate unused tacmach functions.
Pierre-Marie Pédrot
2020-03-24
Merge PR #11858: Rename Retypeops -> Relevanceops
Pierre-Marie Pédrot
2020-03-24
Fix world and watch targets of Makefile.dune now that doc has install rules.
Théo Zimmermann
2020-03-24
Fix deploy of refman following #11855.
Théo Zimmermann
2020-03-24
Run ocamlformat on modified ml / mli files in pre-commit hook.
Théo Zimmermann
2020-03-24
“auto with zarith”: use “lia” rather than “omega”
Vincent Laporte
2020-03-24
[stdlib] Do not rely on failing “auto”
Vincent Laporte
2020-03-24
Merge PR #11892: [refman] Fix caching, which was broken by the addition of co...
Théo Zimmermann
2020-03-23
Merge PR #9607: [ci] add metacoq
Gaëtan Gilbert
2020-03-23
[refman] Fix caching, which was broken by the addition of coq_config
Clément Pit-Claudel
2020-03-23
Fix levels of `<=?` and `<?` in the stdlib
Jason Gross
2020-03-23
[ci] add metacoq
Matthieu Sozeau
2020-03-23
Sorting: Swap the names of Sorted_sort and LocallySorted_sort
Lysxia
2020-03-23
Merge PR #11888: Fix broken links in prodn:: in doc
Théo Zimmermann
2020-03-23
s/magicaly/magically/
Jason Gross
2020-03-23
Merge PR #11867: Fix the computation of recursive principles with let-bindings.
Enrico Tassi
2020-03-23
Merge PR #11442: Add module ZifyPow to avoid compatibility issue with 8.11.
Frédéric Besson
2020-03-22
Format hyperlink targets and link ids with the same name
Jim Fehrle
2020-03-22
[obligations] Don't allocate libobjects for obligation info.
Emilio Jesus Gallego Arias
2020-03-22
[obligations] Small cleanup for open
Emilio Jesus Gallego Arias
2020-03-22
Testing notations which are specific numerals.
Hugo Herbelin
2020-03-22
Adding support for parsing "+" sig in NumTok.
Hugo Herbelin
2020-03-22
Overlay for QuickChick
Hugo Herbelin
2020-03-22
Adding a test for printing single characters.
Hugo Herbelin
2020-03-22
Test-suite: Assume coqtop output is text even with non-printable characters.
Hugo Herbelin
2020-03-22
Centralizing all kinds of numeral string management in numTok.ml.
Hugo Herbelin
2020-03-22
Adding bignat to parse positive numbers; bigint now includes negative ints.
Hugo Herbelin
2020-03-22
Merge PR #11731: [proof] Miscellaneous refactorings
Gaëtan Gilbert
2020-03-22
Merge PR #11851: Process command line load vernaculars before command line Go...
Emilio Jesus Gallego Arias
2020-03-22
Merge PR #11855: Build and install refman with Dune.
Emilio Jesus Gallego Arias
2020-03-22
[proof] Deprecate unused tacmach functions.
Emilio Jesus Gallego Arias
2020-03-21
Add module ZifyPow to avoid compatibility issue with 8.11.
Théo Zimmermann
2020-03-21
Reorder the load/require cmd-options and set/unset cmd-options
Lasse Blaauwbroek
[prev]
[next]