| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2015-01-27 | Doc: Overfull lines in chapter on Canonical Structures. | Hugo Herbelin | |
| 2015-01-25 | Made replacing of text in CoqIDE atomic w.r.t. the undo/redo. | Pierre-Marie Pédrot | |
| 2015-01-25 | Fixing bug #3947. | Pierre-Marie Pédrot | |
| 2015-01-25 | Test for bug #3798. | Pierre-Marie Pédrot | |
| 2015-01-24 | Doc: Fixing some compilation problems with chapter Canonical | Hugo Herbelin | |
| Structures. Text mode + a "Require Import" in a module which provokes suspect warnings "Exception Not_found". | |||
| 2015-01-24 | Updating CHANGES (grammar, thanks to AS for pointing it out) + | Hugo Herbelin | |
| a line on "Intuition Negation Unfolding". | |||
| 2015-01-24 | Removed obsolete option "Legacy Partially Applied Elimination | Hugo Herbelin | |
| Argument" which I used temporarily in a branch to have "destruct eq_dec" working like in v8.4 and not like the "destruct (eq_dec _ _)" of 8.4. I finally made "destruct (eq_dec _ _)" working in 8.5 like "destruct eq_dec" was working in 8.4 (and is still working in 8.5). | |||
| 2015-01-24 | Reference Manual: Documenting new printing of evars and new effect of | Hugo Herbelin | |
| Set Printing Existential Instances (see bug report #3951). | |||
| 2015-01-24 | Equality Schemes options: reverting commit ff9f94634 which is | Hugo Herbelin | |
| obviously inconsistent with the decisions taken in commits 2e8fb20e04da and 0bc569026048 about bugs #2550 and #3606. Now having options Boolean Equality Schemes and Decidable Equality Schemes. | |||
| 2015-01-24 | Isolate a function for printing evar sets. | Hugo Herbelin | |
| 2015-01-24 | Tentative workaround for bug #3798. | Pierre-Marie Pédrot | |
| Ultimately setoid rewrite should be written in the monad to fix it properly. | |||
| 2015-01-23 | Fix previous commit on extraction. | Maxime Dénès | |
| Since name clashes are discovered by side effects, the order of traversal of module structs cannot be changed. | |||
| 2015-01-23 | Typos, grammar, layout in CHANGES (continued). | Hugo Herbelin | |
| 2015-01-23 | Typos, grammar, layout in CHANGES. | Hugo Herbelin | |
| 2015-01-23 | Extraction: fix #3629. | Maxime Dénès | |
| The control flow of extraction is hard to read due to exceptions. When meeting an inlined constant extracted to custom code, they could desynchronize some tables in charge of detecting name clashes, leading to an anomaly. | |||
| 2015-01-21 | Add the possibility of defining opaque terms with program. | mlasson | |
| 2015-01-21 | Reference Manual/Credits: expand the paragraph on the new proof engine to ↵ | Arnaud Spiwack | |
| match the overall style. | |||
| 2015-01-21 | Reference Manual/Credits: native compute is a major contribution. | Arnaud Spiwack | |
| It is, at the very least, listed as such in the overview. So, I moved it to the relevant part and expanded the description with a sentence or two. | |||
| 2015-01-21 | Reference manual/Credits: populate the "various smaller-scale improvements" ↵ | Arnaud Spiwack | |
| part. | |||
| 2015-01-21 | Reference Manual/Credits: remove a duplicate. | Arnaud Spiwack | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |