| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 ↵ | Hugo Herbelin | |
| coqtop mode. | |||
| 2015-02-10 | Fixing #4017, #3726 (use of implicit arguments was lost in multiple variable ↵ | Hugo Herbelin | |
| declarations). | |||
| 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 | |
| safety hole in judge_of_constant_knowing parameters which was not checking the result of the check correctly (the rest of the calls in that file and all of the checker have been checked). | |||
| 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 | |
| This reverts commit 36c7fba1180eaa2ceea7cc486ebd2f0d649042f0. I had mixed up the boolean flag, resulting in the loss of evar-free versions of tactics. | |||
| 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 | |
| We only allow color output under Unix OSes. | |||
| 2015-02-06 | More efficient Richpp. | Pierre-Marie Pédrot | |
| We build the rich XML at once without generating the printed string. | |||
| 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 | |
| Here nonsensical means a Qed/Defined without a Lemma. | |||
| 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 | |
| Strings are at most 16M on 32 bit OCaml, and the system state may be bigger. In this case we write to tmp file and Marshal.from_channel. We can't directly use the channel interface because of badly designed non blocking API (available only on fds and not channels). | |||
| 2015-02-05 | Properly set module names in presence of -Q. (Fix for bug #3958) | Guillaume Melquiond | |
| This is done by adding a fourth type of loadpath, the ones that are neither implicit nor root, for the subdirectories of a -Q root. Note: this means that scanning for available directories is no longer done on the fly for -Q, but once and for all, as with -R. | |||
| 2015-02-04 | Detecting automatically whether .opt versions of ocaml executables exist; | Hugo Herbelin | |
| making configure option -opt deprecated. | |||
| 2015-02-04 | Optimized Import/Export the same way as Require Import/Export was | Hugo Herbelin | |
| optimized. Now "Import Arith ZArith" imports only once the libraries reexported by both Arith and ZArith. (No side effect can be inserted here, so that this looks compatible). | |||
| 2015-02-04 | Fixing bug #3996. | Pierre-Marie Pédrot | |
| 2015-02-04 | More efficient implementation of Richpp. | Pierre-Marie Pédrot | |
| Instead of constructing the XML string and parsing it afterwards, we build it by hijacking the formatting output. | |||
| 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 | |
| This reverts commit 2e09a22baeb93c57e6d8388313dc638349679910. | |||
| 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 | |
| I know it seems wrong but if you call coq to get a path, you are likely to pass it around, and this makes the dir separator of windows "\" disappear immediately being interpreted as an escape character. In cygwin "/" is also understood as a directory separator. | |||
| 2015-02-02 | Removing dead code. | Pierre-Marie Pédrot | |
| 2015-01-29 | Fix index of reference manual. | Guillaume Melquiond | |
| 2015-01-29 | An update on INSTALL.ide. | Hugo Herbelin | |
| 2015-01-29 | Removing outdated INSTALL.macosx file; instructions are more likely to | Hugo Herbelin | |
| be up-to-date on the web. If someone can check that INSTALL.win is up-to-date, that'd be nice. | |||
| 2015-01-29 | Extra check at the INSTALL file. | Hugo Herbelin | |
| 2015-01-29 | Remove spurious "Loading ML file" and "<W> Grammar extension" from the ↵ | Guillaume Melquiond | |
| reference manual. | |||
| 2015-01-29 | Remove some "Warning:" from the reference manual. | Guillaume Melquiond | |
| 2015-01-29 | Prevent spurious warnings about Arguments. | Guillaume Melquiond | |
| The Arguments command tends to emit the following warning even when properly used: This command is just asserting the number and names of arguments of cons. If this is what you want add ': assert' to silence the warning. If you want to clear implicit arguments add ': clear implicits'. If you want to clear notation scopes add ': clear scopes' In fact, even ': assert' does not silence it, contrarily to what the message suggests. | |||
| 2015-01-29 | Made the CoqIDE progress gutter clickable. | Pierre-Marie Pédrot | |
| 2015-01-29 | Fix some typos in the documentation. | Guillaume Melquiond | |
| 2015-01-29 | Fix some broken Coq scripts in the reference manual. | Guillaume Melquiond | |
| 2015-01-28 | Fixing bug #3931. | Pierre-Marie Pédrot | |
| 2015-01-27 | Fixed a wrong warning in coq_makefile. | Pierre Courtieu | |
| A non empty dir detected as an empty one. | |||
| 2015-01-27 | Allow -type-in-type to be an option also for coqc. | Daniel R. Grayson | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |