| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2015-01-21 | Reference manual: pass over the credit section for English. | Arnaud Spiwack | |
| 2015-01-21 | Reference manual: fix typo in doc of [tryif/then/else]. | Arnaud Spiwack | |
| Fixes #3939. | |||
| 2015-01-20 | Fix a critical bug in machine arithmetic for native compiler. | Maxime Dénès | |
| 2015-01-19 | Making unification of LetIn's expressions more consistent (see #3920). | Hugo Herbelin | |
| Unifying two let-in's expresions syntactically is a heuristic (compared to performing the zeta-reduction). This heuristic was requiring unification of types which is too strong for the heuristic to work uniformly since the types might only be related modulo subtyping. The patch is to remove the unification of types, which allows then to have the heuristic work uniformly on the bodies. On the other side, I hope it does not loose (still heuristical) unifications compared to before (presumably, since instantiating the evars in the body will induce constraints for solving potential evars in the types of the let-in bodies, but this would need a proof). Anyway, it is not about correction, it is about a heuristic, which maybe done too early actually. | |||
| 2015-01-18 | Fix a big bug in native_compute tactic: since Hugo's 364decf59c, it was | Maxime Dénès | |
| actually calling the VM at Qed time. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |