| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-02-12 | Capital letter in plugins. | Hugo Herbelin | |
| 2015-02-12 | Using same code for browsing physical directories in coqtop and coqdep. | Hugo Herbelin | |
| In particular: - abstracting the code using calls to Unix opendir, stat, and closedir, - uniformly using warnings when a directory does not exist (coqtop was ignoring silently and coqdep was exiting via handle_unix_error). | |||
| 2015-02-12 | Fixing #3982 (conflict with max notation for universes). | Hugo Herbelin | |
| 2015-02-12 | Fixing #3997 (occur-check in the presence of primitive projections, patch | Hugo Herbelin | |
| from Matthieu). | |||
| 2015-02-12 | Fixing bug #4023. | Pierre-Marie Pédrot | |
| 2015-02-12 | Fixing compilation for 3.12. | Pierre-Marie Pédrot | |
| 2015-02-12 | Tentative fix for bug #4027. | Pierre-Marie Pédrot | |
| 2015-02-12 | Make clearer that "Remove Printing Let" does not influence destructuring let. | Guillaume Melquiond | |
| 2015-02-11 | Adding test for bug #3786. | Pierre-Marie Pédrot | |
| 2015-02-11 | Missing space in error message | Matěj Grabovský | |
| 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 | |
| Probably a regression introduced in some code refactoring. Affects only PIDE based code. | |||
| 2015-02-11 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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 | |
| This is a fixup of commit 2e09a22b that used uniquely generated kernel names but forgot to substitute them. | |||
| 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 ↵ | 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 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |