index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2015-02-11
Win: use .exe extension for the ocaml compiler (Close 3572)
Enrico Tassi
2015-02-11
STM: is Flags.async_proofs_full then always delegate
Enrico Tassi
2015-02-11
Fixing bug #4019, and checker blow-up at once.
Pierre-Marie Pédrot
2015-02-11
Clarifying the implementation of universe hashconsing.
Pierre-Marie Pédrot
2015-02-11
Adding a statistic function on hashconsing tables.
Pierre-Marie Pédrot
2015-02-11
Tactic Notation: use stable unique key for notations (Close: 3970)
Enrico Tassi
2015-02-11
Adding a test-suite for tactic notation naming.
Pierre-Marie Pédrot
2015-02-11
Make coqdoc -l properly handle Local before Ltac. (Fix for bug #3307)
Guillaume Melquiond
2015-02-11
Adding test for bug #3900.
Pierre-Marie Pédrot
2015-02-11
Fixing bug #3900.
Pierre-Marie Pédrot
2015-02-11
Reinstauring backtrace display in CoqIDE.
Pierre-Marie Pédrot
2015-02-10
Avoid html markup inside tex files and fix url.
Guillaume Melquiond
2015-02-10
Run coqdoc on the .v files from the plugins directory. (Fix for bug #2195)
Guillaume Melquiond
2015-02-10
Fixing #4001 (missing type constraints when building return clause of match).
Hugo Herbelin
2015-02-10
Improving further e11854569b8 and 3e5b9ab9f75e4 on when to print goals in coq...
Hugo Herbelin
2015-02-10
Fixing #4017, #3726 (use of implicit arguments was lost in multiple variable ...
Hugo Herbelin
2015-02-10
Fixing #4018 (uncaught exception on non-equality in intros [=]).
Hugo Herbelin
2015-02-10
A few refinements in whodidwhat 8.4.
Hugo Herbelin
2015-02-10
Fix typeops ignoring results of check functions with let _, and one
Matthieu Sozeau
2015-02-10
Add section numbering to the refman PDF. (Fix for bug #2365)
Guillaume Melquiond
2015-02-10
Prevent Latex from messing with backticks. (Fix for bug #3871)
Guillaume Melquiond
2015-02-10
Fix documentation of generalize. (Fix for bug #4015)
Guillaume Melquiond
2015-02-10
Fix some documentation typo.
Guillaume Melquiond
2015-02-10
Granting wish #4008.
Pierre-Marie Pédrot
2015-02-10
Test for bug #4012.
Pierre-Marie Pédrot
2015-02-10
More expressive API for tclWITHHOLES.
Pierre-Marie Pédrot
2015-02-10
Making undo/redo atomic in CoqIDE.
Pierre-Marie Pédrot
2015-02-10
Revert "Removing spurious tclWITHHOLES."
Pierre-Marie Pédrot
2015-02-09
Fix bug #4014.
Pierre-Marie Pédrot
2015-02-07
STM: tolerate simple side effects in async proofs (Close: 4006)
Enrico Tassi
2015-02-07
Fixing bug #4009.
Pierre-Marie Pédrot
2015-02-06
More efficient Richpp.
Pierre-Marie Pédrot
2015-02-05
Windows: open .vo files in binary mode
Enrico Tassi
2015-02-05
Fix some documentation typos.
Guillaume Melquiond
2015-02-05
Fix automatic undo after nonsensical Qed in tty mode (Close: 3980)
Enrico Tassi
2015-02-05
Windows installer cleanup
Enrico Tassi
2015-02-05
Marshal.from_string on 32 bit systems use tmpfile if needed (Close: 3968)
Enrico Tassi
2015-02-05
Properly set module names in presence of -Q. (Fix for bug #3958)
Guillaume Melquiond
2015-02-04
Detecting automatically whether .opt versions of ocaml executables exist;
Hugo Herbelin
2015-02-04
Optimized Import/Export the same way as Require Import/Export was
Hugo Herbelin
2015-02-04
Fixing bug #3996.
Pierre-Marie Pédrot
2015-02-04
More efficient implementation of Richpp.
Pierre-Marie Pédrot
2015-02-04
Tactic Notation: use stable unique key for notations (Close: 3970)
Enrico Tassi
2015-02-04
CThread: workaround for threads lockup on windwos made more aggressive
Enrico Tassi
2015-02-04
Nativelib: catch Unix_error (like no ocamlopt found)
Enrico Tassi
2015-02-03
Revert "Tactic Notation: use stable unique key for notations (Close: 3970)"
Enrico Tassi
2015-02-03
Tactic Notation: use stable unique key for notations (Close: 3970)
Enrico Tassi
2015-02-03
spit module path using / as directory separator
Enrico Tassi
2015-02-02
Removing dead code.
Pierre-Marie Pédrot
2015-01-29
Fix index of reference manual.
Guillaume Melquiond
[next]