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-25
Merge PR #13674: Enhance the performance of the move tactic
HEAD
master
coqbot-app[bot]
2021-04-23
Merge PR #14075: New level of abstraction for streams with (non-canonical) lo...
Pierre-Marie Pédrot
2021-04-23
Merge PR #14158: Provide a reinit data for Ltac2 notations with entry level 4.
coqbot-app[bot]
2021-04-23
Merge PR #14041: Enable canonical fun _ => _ projections.
coqbot-app[bot]
2021-04-23
Merge PR #13965: [abbreviation] user syntax to set interp scope of argument
Pierre-Marie Pédrot
2021-04-23
Merge PR #14161: test-suite: add approve-coqdoc to update all coqdoc output f...
coqbot-app[bot]
2021-04-23
Overlay for elpi.
Hugo Herbelin
2021-04-23
Relying on the abstract notion of streams with location for parsing.
Hugo Herbelin
2021-04-23
Locations: Moving functions Ploc.sub and Ploc.after to loc.ml.
Hugo Herbelin
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-23
test-suite: add approve-coqdoc to update all coqdoc output files at once.
Hugo Herbelin
2021-04-23
Provide a reinit data for Ltac2 notations with entry level 4.
Pierre-Marie Pédrot
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-22
Add changelog
Pierre Roux
2021-04-22
Extend Canonical Structure documentation.
Jan-Oliver Kaiser
2021-04-22
Enable canonical `fun _ => _` projections.
Jan-Oliver Kaiser
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
More efficient variable membership check for Logic.move.
Pierre-Marie Pédrot
2021-04-20
Do not construct intermediate lists in Logic.move.
Pierre-Marie Pédrot
2021-04-20
Specialize the code of Logic.move.
Pierre-Marie Pédrot
2021-04-20
Preserve the context_val structure as much as possible in Logic.move.
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
[next]