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
*
Bump year in headers.
Maxime Dénès
2017-06-01
*
Merge PR#693: A subtle bug in tclWITHHOLES.
Maxime Dénès
2017-05-30
|
\
*
\
Merge PR#695: Omega: fix bug #4132
Maxime Dénès
2017-05-30
|
\
\
|
*
|
Omega: use "simpl" only on coefficents, not on atoms (fix #4132)
Pierre Letouzey
2017-05-29
|
/
/
*
|
Merge PR#685: Fix a bug in checker
Maxime Dénès
2017-05-29
|
\
\
*
\
\
Merge PR#546: Fix for bug #4499 and other minor related bugs
Maxime Dénès
2017-05-29
|
\
\
\
|
|
*
|
Fix a bug in checker
Amin Timany
2017-05-28
|
|
/
/
|
/
|
|
|
|
*
Fixing a subtle bug in tclWITHHOLES.
Hugo Herbelin
2017-05-28
|
|
/
|
/
|
*
|
Merge PR#679: Bug 5546, qualify datatype constructors when needed in Show Match
Maxime Dénès
2017-05-28
|
\
\
*
\
\
Merge PR#634: Fix bug #5526, don't check for nonlinearity in notation if prin...
Maxime Dénès
2017-05-26
|
\
\
\
*
\
\
\
Merge PR#672: Add parsers-examples target to fiat-parsers ci
Maxime Dénès
2017-05-26
|
\
\
\
\
|
|
|
*
|
Bug 5546, qualify datatype constructors when needed
Paul Steckler
2017-05-25
*
|
|
|
|
Merge PR#416: Fix the way setoid_rewrite handles bindings.
Maxime Dénès
2017-05-25
|
\
\
\
\
\
|
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
*
|
|
Add parsers-examples target to fiat-parsers ci
Jason Gross
2017-05-23
|
|
/
/
/
|
/
|
|
|
|
*
|
|
Fix bindings handling of setoid_rewrite.
Cyprien Mangin
2017-05-23
|
/
/
/
*
|
|
Merge PR#653: Bug #5535, test for Show with -emacs
Maxime Dénès
2017-05-20
|
\
\
\
*
\
\
\
Merge PR#641: Fix bug #5486, don't reverse ids in tuples
Maxime Dénès
2017-05-20
|
\
\
\
\
|
|
*
|
|
add test for Show with -emacs, bug 5535
Paul Steckler
2017-05-19
|
|
/
/
/
|
/
|
|
|
|
|
*
|
Fixing bug #5526,allow nonlinear variables in Notation patterns
Paul Steckler
2017-05-17
|
*
|
|
fix swapping of ids in tuples, bug 5486
Paul Steckler
2017-05-17
|
/
/
/
*
|
|
Merge PR#635: Fixing #5522 (anomaly with free vars of pat)
Maxime Dénès
2017-05-17
|
\
\
\
|
*
|
|
Fixing bug #5222 (anomaly with "`pat" in the presence of scope delimiters).
Hugo Herbelin
2017-05-16
|
*
|
|
Fixing a bug with nested "as" clauses in "match".
Hugo Herbelin
2017-05-16
*
|
|
|
Merge PR#624: Switch bedrock to mit-plv base
Maxime Dénès
2017-05-16
|
\
\
\
\
|
|
/
/
/
|
/
|
|
|
*
|
|
|
Removing a line warned unused.
Hugo Herbelin
2017-05-14
*
|
|
|
Removing a variable warned unused.
Hugo Herbelin
2017-05-14
|
|
/
/
|
/
|
|
|
*
|
Switch bedrock to mit-plv base
Jason Gross
2017-05-10
|
/
/
*
|
Merge PR#604: FIx bug #5300: Anomaly: Uncaught exception Not_found" in "Print...
Maxime Dénès
2017-05-10
|
\
\
*
\
\
Merge PR#591: Add bmsherman/topology to the ci
Maxime Dénès
2017-05-09
|
\
\
\
|
*
|
|
Put .travis.yml in alphabetical order
Jason Gross
2017-05-09
*
|
|
|
Merge PR#609: Fix bug #3659: -time should understand multibyte encodings.
Maxime Dénès
2017-05-09
|
\
\
\
\
|
*
|
|
|
Fix bug #3659: -time should understand multibyte encodings.
Pierre-Marie Pédrot
2017-05-05
|
/
/
/
/
|
|
*
/
FIx bug #5300: uncaught exception in "Print Assumptions".
Cyprien Mangin
2017-05-03
|
|
/
/
|
/
|
|
*
|
|
Merge PR#603: Fix outdated description in RefMan.
Maxime Dénès
2017-05-03
|
\
\
\
|
*
|
|
Fix outdated description in RefMan.
Théo Zimmermann
2017-05-03
|
/
/
/
*
|
|
Merge PR#597: Fixing #5487 (v8.5 regression on ltac-matching expressions with...
Maxime Dénès
2017-05-02
|
\
\
\
*
\
\
\
Merge PR#589: remove unneeded -emacs flag in coq-prog-args in test-suite files
Maxime Dénès
2017-05-02
|
\
\
\
\
*
\
\
\
\
Merge PR#599: Repairing `Set Rewriting Schemes`
Maxime Dénès
2017-05-02
|
\
\
\
\
\
*
|
|
|
|
|
Avoiding registering files from _build_ci when not calling Makefile.ci.
Hugo Herbelin
2017-05-02
|
|
|
|
*
|
Add bmsherman/topology to the ci
Jason Gross
2017-05-01
|
|
_
|
_
|
/
/
|
/
|
|
|
|
|
*
|
|
|
Fixing Set Rewriting Schemes bugs introduced in v8.5.
Hugo Herbelin
2017-05-01
|
/
/
/
/
|
*
|
|
remove unneeded -emacs flag to coq-prog-args
Paul Steckler
2017-05-01
|
|
*
|
Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).
Hugo Herbelin
2017-05-01
|
|
*
|
Really fixing #2602 which was wrongly working because of #5487 hiding the cause.
Hugo Herbelin
2017-05-01
|
|
/
/
|
/
|
|
*
|
|
Answer to db28e827d: I did test the commit on test-suite but for some
Hugo Herbelin
2017-05-01
*
|
|
Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions with evars)."
Maxime Dénès
2017-04-28
|
/
/
*
|
Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).
Hugo Herbelin
2017-04-28
*
|
Merge PR#587: Fix description of command-line arguments for Add (Rec) LoadPath
Maxime Dénès
2017-04-27
|
\
\
|
*
|
fix order of command-line arguments mentioned in Add LoadPath
Paul Steckler
2017-04-27
|
/
/
*
|
Test for bug #5193: Uncaught exception Class_tactics.Search.ReachedLimitEx.
Pierre-Marie Pédrot
2017-04-27
[next]