index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2017-01-20
Do not add redundant side effects in tactic code.
Pierre-Marie Pédrot
2017-01-17
Mapping named_context_val preserves sharing when possible.
Pierre-Marie Pédrot
2017-01-17
STM: fix run-time classification of VernacInstance (fix #5313)
Enrico Tassi
2017-01-16
Fixing (part of) #5303 (clarifications around Record/Structure/Variant).
Hugo Herbelin
2017-01-13
Fix race condition in STM DAG generation (in debug mode).
Maxime Dénès
2017-01-13
Properly remove aux files in subdirectories (bug #5089).
Erik Martin-Dorel
2017-01-13
Fix broken .aux machinery.
Guillaume Melquiond
2017-01-12
Fix configure crash on some version strings of camlp5, e.g. "6.18-exp" (bug #...
Guillaume Melquiond
2017-01-04
Fixing another inconsistency when looking for camlp5o when camlp5dir is given.
Hugo Herbelin
2016-12-28
Fix some typos in tutorial (bug #5294).
Guillaume Melquiond
2016-12-23
Handle application of a primitive projection to a not yet evaluated cofixpoin...
Guillaume Melquiond
2016-12-19
Avoid concurrent runs when producing html documentation (bug #5269).
Guillaume Melquiond
2016-12-16
Fix incorrect documentation that prevents successful compilation (bug #5265).
Guillaume Melquiond
2016-12-08
Set version to 8.6 in configure.
Maxime Dénès
2016-12-08
Windows build scripts for 8.6 final.
Maxime Dénès
2016-12-08
Fix paths in 32-bit windows build scripts.
Maxime Dénès
2016-12-07
Commit bumping the version number was partial...
Maxime Dénès
2016-12-07
Add bat files for 8.6rc1 build.
Maxime Dénès
2016-12-07
Add bat files for 8.6beta1 build.
Maxime Dénès
2016-12-07
Set version number to 8.6rc1.
Maxime Dénès
2016-12-07
A few words in CHANGES.
Maxime Dénès
2016-12-07
ssrmatching: fix iter_constr_LR iterator wrt Proj
Enrico Tassi
2016-12-06
Fix #5248 - test-suite fails in 8.6beta1
Maxime Dénès
2016-12-06
Fix broken documentation in presence of \zeroone{... \tt ...}.
Guillaume Melquiond
2016-12-06
Update documentation (bugs #5246 and #5251).
Guillaume Melquiond
2016-12-06
Merge remote-tracking branch 'github/pr/387' into v8.6
Maxime Dénès
2016-12-06
Merge remote-tracking branch 'github/pr/389' into v8.6
Maxime Dénès
2016-12-05
Change module for Coq loop
Paul Steckler
2016-12-05
the -byte option is deprecated
Paul Steckler
2016-12-05
ssrmatching: handle primite projections (fix: #5247)
Enrico Tassi
2016-12-05
Compute dependency of C files only in kernel/byterun.
Maxime Dénès
2016-12-04
Merge remote-tracking branch 'github/pr/366' into v8.6
Maxime Dénès
2016-12-04
Merge remote-tracking branch 'github/pr/378' into v8.6
Maxime Dénès
2016-12-02
Fix test-suite after change in "context" printing.
Maxime Dénès
2016-12-02
Document changes
Matthieu Sozeau
2016-12-02
Merge remote-tracking branch 'github/pr/377' into v8.6
Maxime Dénès
2016-12-02
Merge remote-tracking branch 'github/pr/372' into v8.6
Maxime Dénès
2016-12-02
Merge remote-tracking branch 'github/pr/368' into v8.6
Maxime Dénès
2016-12-02
Merge branch 'pr/367' into v8.6
Maxime Dénès
2016-12-02
Fixing lexing of strings in comments for beautifier.
Hugo Herbelin
2016-12-02
Fixing printing of "ltac:" in tactics after surrounding parentheses
Hugo Herbelin
2016-12-02
Comment on universe handling in Parameters
Matthieu Sozeau
2016-12-02
Univs: fix bug #5188
Matthieu Sozeau
2016-12-02
Merge remote-tracking branch 'github/pr/381' into v8.6
Maxime Dénès
2016-12-02
Fix #5242 - Dubious unsilenceable warning on invalid identifier
Maxime Dénès
2016-12-02
Fixing printing of "Set Warnings Append".
Hugo Herbelin
2016-12-02
Fixing space in printing "Context".
Hugo Herbelin
2016-12-02
Fixing printers for pr_auto_using and pr_firstorder_using.
Hugo Herbelin
2016-12-02
Fixing space in printing several list of implicit arguments.
Hugo Herbelin
2016-12-02
Fixing printing of "only parsing" in abbreviations.
Hugo Herbelin
[next]