| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | Merge branch 'v8.5' | 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-28 | Several reproduction cases for the test suite. | Xavier Clerc | |
| 2015-01-28 | Several reproduction cases for the test suite. | Xavier Clerc | |
| 2015-01-27 | Adding a test for bug #3957. | Pierre-Marie Pédrot | |
| 2015-01-27 | Tentative fix for bug #3957. | Pierre-Marie Pédrot | |
| Now that ML tactics are not dispatched according to the type of their arguments anymore, one has to take care of the way potentially atomic tactics are handled. This patch ensures that the atomic tactics generated by the TACTIC EXTEND macro have the right length and the right order. There may be very rare trouble if two ML tactics in the same entry are of the form "foo" x1 ... xn "foo" y1 ... ym where all xi and yi may be empty. I doubt that the legacy implementation behaved well in this case anyway. | |||
| 2015-01-27 | Fixed a wrong warning in coq_makefile. | Pierre Courtieu | |
| A non empty dir detected as an empty one. | |||
| 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 | Equipping extended maps with fold operator defined for any monad. | Pierre-Marie Pédrot | |
| 2015-01-25 | Merge branch 'v8.5' into trunk. | Pierre-Marie Pédrot | |
| 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 | Adding a proper interface to Newring. | Pierre-Marie Pédrot | |
| The ring ASTs were put in a separate interface, and only the extension-related code was put in a dedicated G_newring file. | |||
| 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 | Splitting ML tactics in one function per grammar entry. | Pierre-Marie Pédrot | |
| Furthermore, ML tactic dispatch is not done according to the type of its argument anymore. | |||
| 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 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |