index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2021-04-23
LStream: a library for streams with non-canonical locations.
Hugo Herbelin
2021-04-23
Gramlib: token_ematch has a useless argument.
Hugo Herbelin
2021-04-22
Merge PR #14128: Uniformize the name of the Ltac2 boolean equality function.
coqbot-app[bot]
2021-04-22
Merge PR #14143: Add mczify to CI
coqbot-app[bot]
2021-04-21
Merge PR #14094: Properly pass the Ltac2 notation level to the gramlib API.
coqbot-app[bot]
2021-04-21
Merge PR #13911: Remove the :> type cast?
coqbot-app[bot]
2021-04-21
Add mczify to CI
Kazuhiko Sakaguchi
2021-04-20
Merge PR #14133: Slightly tweak the not-unit Ltac2 warning.
coqbot-app[bot]
2021-04-20
Merge PR #14131: Check for existence before using `Global.lookup_constant` in...
Pierre-Marie Pédrot
2021-04-20
Merge PR #14089: unify for Ltac2
Pierre-Marie Pédrot
2021-04-19
Merge PR #14068: [build] Remove leftovers of code signing / OSX IDE infrastru...
coqbot-app[bot]
2021-04-19
changelog entry for Ltac2 unify
Samuel Gruetter
2021-04-19
Merge PR #14060: Coqide: on MacOS X, allow the command (⌘) key to be set/un...
Pierre-Marie Pédrot
2021-04-19
[build] Remove leftovers of codesigning / OSX IDe infrastructure.
Emilio Jesus Gallego Arias
2021-04-19
Merge PR #14108: [zify] bugfix
Vincent Laporte
2021-04-19
Check for existence before using `Global.lookup_constant` instead of catching...
Lasse Blaauwbroek
2021-04-19
Slightly tweak the not-unit Ltac2 warning.
Pierre-Marie Pédrot
2021-04-19
Merge PR #13846: Include (* ... *) comments in .. coqtop:: directives in Sphi...
coqbot-app[bot]
2021-04-19
Merge PR #13815: Improve description of conversions
coqbot-app[bot]
2021-04-18
Coqide: on MacOS X, allow the command key to be set/unset as a modifier.
Hugo Herbelin
2021-04-18
Merge PR #14122: Remove macOS dmg build.
coqbot-app[bot]
2021-04-18
Merge PR #14115: Change `Coqlib.lib_ref` to fail with `NameNotRegistered` ins...
coqbot-app[bot]
2021-04-18
Merge PR #14127: Pin docutils to 0.16.
coqbot-app[bot]
2021-04-18
Merge PR #14112: Cleanup useless environment manipulation in Class declaration
coqbot-app[bot]
2021-04-17
Uniformize the name of the Ltac2 boolean equality function.
Pierre-Marie Pédrot
2021-04-17
Improve conversion chapter.
Jim Fehrle
2021-04-17
Disambiguate move tactics.
Jim Fehrle
2021-04-17
Include (* ... *) comments in .. coqtop:: directives in Sphinx output
Jim Fehrle
2021-04-17
Pin docutils to 0.16.
Théo Zimmermann
2021-04-17
Remove superfluous sort.
Jim Fehrle
2021-04-17
Properly pass the Ltac2 notation level to the gramlib API.
Pierre-Marie Pédrot
2021-04-16
[zify] bugfix
Frederic Besson
2021-04-16
Merge PR #13939: Allow scope delimiters in Ltac2 open_constr:(...) quotation.
coqbot-app[bot]
2021-04-16
Remove macOS dmg build.
Théo Zimmermann
2021-04-16
Catch UserError in Hipattern.match_with_equation in case name is not yet regi...
Lasse Blaauwbroek
2021-04-15
Merge PR #14111: [ci] update elpi to 1.13.1
coqbot-app[bot]
2021-04-14
Update dev/ci/user-overlays/14111-gares-update-elpi.sh
Enrico Tassi
2021-04-14
Merge PR #14050: Remove remote counter system
coqbot-app[bot]
2021-04-14
overlay file
Enrico Tassi
2021-04-14
Merge PR #14045: Zify: more aggressive application of saturation rules
Vincent Laporte
2021-04-14
Cleanup useless environment manipulation in Class declaration
Gaëtan Gilbert
2021-04-14
Add test for -schedule-vio-checking
Gaëtan Gilbert
2021-04-14
Overlay for no remote counter
Gaëtan Gilbert
2021-04-14
Remove remote counter system
Gaëtan Gilbert
2021-04-14
Put async worker id in universe names
Gaëtan Gilbert
2021-04-14
[ci] update elpi to 1.13.1
Enrico Tassi
2021-04-13
Merge PR #14024: [coqdep] error on non-existent and unreadable files
coqbot-app[bot]
2021-04-12
[zify] More aggressive application of saturation rules
BESSON Frederic
2021-04-12
[coqdep] error on non-existent and unreadable files
Hendrik Tews
2021-04-12
Fix unknown -vos option for coqdep_boot introduced in PR #11074
Hendrik Tews
[next]