index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
dev
Commit message (
Expand
)
Author
Age
*
Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.
Maxime Dénès
2017-12-14
|
\
*
|
Revert "[ci] Temporal workaround for checker non-backwards compatible change."
Théo Zimmermann
2017-12-12
*
|
Merge PR #6331: Linter: skip PRs older than the linter.
Maxime Dénès
2017-12-11
|
\
\
*
\
\
Merge PR #6368: [api] Remove yet another type alias.
Maxime Dénès
2017-12-11
|
\
\
\
*
\
\
\
Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.
Maxime Dénès
2017-12-11
|
\
\
\
\
*
\
\
\
\
Merge PR #6358: [ci] Download ci-sf archives into the proper CI build dir.
Maxime Dénès
2017-12-11
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #6351: Fix a copy-paste error in ci-ltac2.
Maxime Dénès
2017-12-11
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #6346: [ci] CoLoR has moved to github
Maxime Dénès
2017-12-11
|
\
\
\
\
\
\
\
|
|
|
|
|
|
|
*
[build] Remove coqmktop in favor of ocamlfind.
Emilio Jesus Gallego Arias
2017-12-10
*
|
|
|
|
|
|
|
[ci] Temporal workaround for checker non-backwards compatible change.
Emilio Jesus Gallego Arias
2017-12-10
|
|
|
|
|
*
|
|
[api] Remove yet another type alias.
Emilio Jesus Gallego Arias
2017-12-09
|
|
_
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
*
[lib] Rename Profile to CProfile
Emilio Jesus Gallego Arias
2017-12-09
|
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
*
|
|
[ci] Download ci-sf archives into the proper CI build dir.
Emilio Jesus Gallego Arias
2017-12-09
|
|
_
|
/
/
/
|
/
|
|
|
|
|
|
*
|
|
Fix a copy-paste error in ci-ltac2.
Théo Zimmermann
2017-12-08
*
|
|
|
|
Merge PR #6158: Allows a level in the raw and glob printers
Maxime Dénès
2017-12-08
|
\
\
\
\
\
|
|
*
|
|
|
[ci] CoLoR has moved to github
Emilio Jesus Gallego Arias
2017-12-07
*
|
|
|
|
|
Merge PR #6267: Fix PR merge script.
Maxime Dénès
2017-12-07
|
\
\
\
\
\
\
|
|
_
|
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
*
|
Overlay for Equations.
Gaëtan Gilbert
2017-12-06
|
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
|
*
Linter: skip PRs older than the linter.
Gaëtan Gilbert
2017-12-06
|
|
_
|
_
|
/
|
/
|
|
|
*
|
|
|
uninstall doc dir, not dev (which is not installed), #6007
Paul Steckler
2017-12-01
*
|
|
|
Merge PR #736: [ci] Test coqchk on the CompCert target.
Maxime Dénès
2017-12-01
|
\
\
\
\
*
\
\
\
\
Merge PR #6244: [lib] [api] Introduce record for `object_prefix`
Maxime Dénès
2017-11-30
|
\
\
\
\
\
|
|
*
|
|
|
[ci] Test coqchk on the CompCert target.
Théo Zimmermann
2017-11-30
|
|
/
/
/
/
|
/
|
|
|
|
*
|
|
|
|
Merge PR #6269: [ci] [vst] Shorten compilation time to avoid Travis timeouts.
Maxime Dénès
2017-11-30
|
\
\
\
\
\
|
|
|
*
|
|
Fix usage comment.
Théo Zimmermann
2017-11-29
|
|
|
*
|
|
This script apparently uses bash-specific features.
Théo Zimmermann
2017-11-29
|
|
|
*
|
|
Fix PR merge script.
Théo Zimmermann
2017-11-29
|
|
_
|
/
/
/
|
/
|
|
|
|
|
|
*
|
|
[lib] [api] Introduce record for `object_prefix`
Emilio Jesus Gallego Arias
2017-11-29
|
|
|
|
/
|
|
|
/
|
*
|
|
|
Add PR backport script.
Théo Zimmermann
2017-11-28
|
*
|
|
[ci] [vst] Shorten compilation time to avoid Travis timeouts.
Emilio Jesus Gallego Arias
2017-11-28
|
/
/
/
*
|
|
Merge PR #6259: Add PR merge script.
Maxime Dénès
2017-11-28
|
\
\
\
|
*
|
|
Add PR merge script.
Maxime Dénès
2017-11-28
|
|
/
/
*
|
|
Merge PR #1033: Universe binder improvements
Maxime Dénès
2017-11-28
|
\
\
\
*
\
\
\
Merge PR #6248: [api] Remove aliases of `Evar.t`
Maxime Dénès
2017-11-28
|
\
\
\
\
|
|
_
|
/
/
|
/
|
|
|
|
|
|
*
Adding overlay for ltac2.
Hugo Herbelin
2017-11-27
*
|
|
|
Merge PR #6227: Linter: do not lint untracked files.
Maxime Dénès
2017-11-27
|
\
\
\
\
|
|
_
|
_
|
/
|
/
|
|
|
|
|
*
|
[api] Remove aliases of `Evar.t`
Emilio Jesus Gallego Arias
2017-11-26
|
|
/
/
|
/
|
|
|
|
*
Overlay for stronger restrict_universe_context.
Gaëtan Gilbert
2017-11-25
|
|
/
|
/
|
*
|
Merge PR #876: In omega or romega, recognizing Z and nat modulo conversion
Maxime Dénès
2017-11-24
|
\
\
*
\
\
Merge PR #6197: [plugin] Remove LocalityFixme über hack.
Maxime Dénès
2017-11-24
|
\
\
\
*
\
\
\
Merge PR #6186: [api] Miscellaneous consolidation.
Maxime Dénès
2017-11-23
|
\
\
\
\
|
|
|
|
*
Linter: do not lint untracked files.
Gaëtan Gilbert
2017-11-23
|
|
_
|
_
|
/
|
/
|
|
|
|
|
|
*
Adding ad hoc overlay for sf/vfa.
Hugo Herbelin
2017-11-23
|
|
_
|
/
|
/
|
|
*
|
|
Merge PR #6189: Disable whitespace linter for .out files.
Maxime Dénès
2017-11-23
|
\
\
\
|
|
|
*
[plugin] Remove LocalityFixme über hack.
Emilio Jesus Gallego Arias
2017-11-22
|
|
_
|
/
|
/
|
|
|
|
*
[api] Miscellaneous consolidation + moves to engine.
Emilio Jesus Gallego Arias
2017-11-21
|
|
/
|
/
|
*
|
[printing] Deprecate all printing functions accessing the global proof.
Emilio Jesus Gallego Arias
2017-11-21
*
|
Merge PR #6185: [parser] Remove unnecessary statically initialized hook.
Maxime Dénès
2017-11-21
|
\
\
*
\
\
Merge PR #6168: Add Equations to CI
Maxime Dénès
2017-11-21
|
\
\
\
|
|
|
*
Disable whitespace linter for .out files.
Gaëtan Gilbert
2017-11-20
[next]
Maxime Dénès
Théo Zimmermann
Emilio Jesus Gallego Arias
Gaëtan Gilbert
Paul Steckler
Hugo Herbelin