index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Fixing unexpected "noise" introduced in commit 24d5448c.
Hugo Herbelin
2016-10-06
*
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-05
|
\
*
|
Fix a bug of Mltop.declare_cache_object.
Pierre-Marie Pédrot
2016-10-05
*
|
Clean up type classes flags and update compat file.
Maxime Dénès
2016-10-05
*
|
Fixing a beautifier bug pointed out by Emilio.
Hugo Herbelin
2016-10-05
*
|
Fix incorrect token description for bullets.
Guillaume Melquiond
2016-10-05
*
|
Revert "Move bullet detection from lexer to parser (bug #5102)."
Guillaume Melquiond
2016-10-05
*
|
Fix #5048 - Casts in pattern raise an anomaly in Constrintern.
Maxime Dénès
2016-10-04
*
|
Quick fix to #4595 (making notations containing "ltac:" unused for printing).
Hugo Herbelin
2016-10-04
*
|
Changing the separator for appended string options to comma.
Maxime Dénès
2016-10-04
*
|
Merge remote-tracking branch 'github/pr/305' into v8.6
Maxime Dénès
2016-10-04
|
\
\
|
|
*
Fixing #4970 (confusion between special "{" and non special "{{" in notations).
Hugo Herbelin
2016-10-03
*
|
|
Merge remote-tracking branch 'github/pr/263' into v8.6
Maxime Dénès
2016-10-03
|
\
\
\
*
|
|
|
Document change related to Keep Proof Equalities in CHANGES.
Maxime Dénès
2016-10-03
*
|
|
|
Merge remote-tracking branch 'github/pr/304' into v8.6
Maxime Dénès
2016-10-03
|
\
\
\
\
|
*
|
|
|
fixing bug 4609: document an option governing the generation of equalities
Yves Bertot
2016-10-03
|
/
/
/
/
*
|
|
|
More tests for tactic "subst".
Hugo Herbelin
2016-10-02
*
|
|
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-02
|
\
\
\
\
|
|
|
_
|
/
|
|
/
|
|
*
|
|
|
Move bullet detection from lexer to parser (bug #5102).
Guillaume Melquiond
2016-10-02
*
|
|
|
Fix bug #5069: Scheme Equality gives anomalies in sections.
Pierre-Marie Pédrot
2016-10-02
*
|
|
|
Fix bug #5087: Improve the error message on record with duplicated fields.
Pierre-Marie Pédrot
2016-10-02
*
|
|
|
Fix bug #4661: Cannot mask the absolute name.
Pierre-Marie Pédrot
2016-10-01
*
|
|
|
Speed up the Search commands.
Guillaume Melquiond
2016-10-01
*
|
|
|
Micro refactoring: use exact_no_check.
Théo Zimmermann
2016-10-01
|
|
|
*
Add command 'Set foo Append "bar"' for appending to an option (bug #5109).
Guillaume Melquiond
2016-10-01
|
|
|
*
Allow appending to string options.
Guillaume Melquiond
2016-10-01
|
|
_
|
/
|
/
|
|
|
*
|
Quick fix to another bug of "subst" introduced in 4e3d464 and spotted by Maxime.
Hugo Herbelin
2016-09-30
*
|
|
Fix bug #5045: [generalize] creates ill-typed terms in 8.6.
Pierre-Marie Pédrot
2016-09-30
*
|
|
Fix bug #4471: [generalize dependent] permits ill-typed terms in trunk.
Pierre-Marie Pédrot
2016-09-30
*
|
|
coqc: recognize -profile-ltac-cutoff
Enrico Tassi
2016-09-30
*
|
|
test-suite/output-modulo-time made more robust
Enrico Tassi
2016-09-30
*
|
|
Merge remote-tracking branch 'github/pr/303' into v8.6
Maxime Dénès
2016-09-30
|
\
\
\
*
\
\
\
Merge remote-tracking branch 'github/pr/299' into v8.6
Maxime Dénès
2016-09-30
|
\
\
\
\
*
\
\
\
\
Merge branch 'v8.5' into v8.6
Maxime Dénès
2016-09-30
|
\
\
\
\
\
|
|
|
_
|
/
/
|
|
/
|
|
|
|
*
|
|
|
Fix test-suite.
Maxime Dénès
2016-09-30
*
|
|
|
|
Merge remote-tracking branch 'github/pr/302' into v8.6
Maxime Dénès
2016-09-30
|
\
\
\
\
\
*
\
\
\
\
\
Merge remote-tracking branch 'github/pr/281' into v8.6
Maxime Dénès
2016-09-30
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge remote-tracking branch 'github/pr/280' into v8.6
Maxime Dénès
2016-09-30
|
\
\
\
\
\
\
\
*
|
|
|
|
|
|
|
Restore code ignoring <W> lines in output (camlp5 warnings)
Enrico Tassi
2016-09-30
*
|
|
|
|
|
|
|
Ignore file names in warning emitted by test-suite/output/* (#5111)
Enrico Tassi
2016-09-30
*
|
|
|
|
|
|
|
In <= 8.5 compat accept "Arguments f /" even if f has arguments (#5112)
Enrico Tassi
2016-09-30
*
|
|
|
|
|
|
|
Give name to warning added in (fdfcdc): arguments-ignore-rename-nonimpl
Enrico Tassi
2016-09-30
|
|
|
|
*
|
|
|
Merge remote-tracking branch 'github/pr/294' into v8.5
Maxime Dénès
2016-09-30
|
|
|
|
|
\
\
\
\
*
|
|
|
|
\
\
\
\
Merge remote-tracking branch 'github/pr/257' into v8.6
Maxime Dénès
2016-09-30
|
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
Merge branch 'v8.5' into v8.6
Maxime Dénès
2016-09-30
|
\
\
\
\
\
\
\
\
\
\
|
|
|
_
|
_
|
_
|
/
/
/
/
/
|
|
/
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
Merge branch '4762' into v8.5
Maxime Dénès
2016-09-30
|
|
\
\
\
\
\
\
\
\
\
|
|
*
|
|
|
|
|
|
|
|
Fix #4762.
Cyprien Mangin
2016-09-30
|
|
|
|
|
|
|
|
|
*
|
LtacProf cutoff is for total percent, not time
Jason Gross
2016-09-29
|
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
Set the default LtacProf cutoff to 2%
Jason Gross
2016-09-29
|
|
_
|
_
|
_
|
_
|
/
/
/
/
|
/
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
Fix bug #4798: compat notations should not modify the parser.
Pierre-Marie Pédrot
2016-09-29
[next]
Hugo Herbelin
Pierre-Marie Pédrot
Maxime Dénès
Guillaume Melquiond
Yves Bertot
Théo Zimmermann
Enrico Tassi
Cyprien Mangin
Jason Gross