aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Making undo/redo atomic in CoqIDE.Gravatar Pierre-Marie Pédrot2015-02-10
|
* Revert "Removing spurious tclWITHHOLES."Gravatar Pierre-Marie Pédrot2015-02-10
| | | | | | | This reverts commit 36c7fba1180eaa2ceea7cc486ebd2f0d649042f0. I had mixed up the boolean flag, resulting in the loss of evar-free versions of tactics.
* Fix bug #4014.Gravatar Pierre-Marie Pédrot2015-02-09
|
* STM: tolerate simple side effects in async proofs (Close: 4006)Gravatar Enrico Tassi2015-02-07
|
* Fixing bug #4009.Gravatar Pierre-Marie Pédrot2015-02-07
| | | | We only allow color output under Unix OSes.
* More efficient Richpp.Gravatar Pierre-Marie Pédrot2015-02-06
| | | | We build the rich XML at once without generating the printed string.
* Windows: open .vo files in binary modeGravatar Enrico Tassi2015-02-05
|
* Fix some documentation typos.Gravatar Guillaume Melquiond2015-02-05
|
* Fix automatic undo after nonsensical Qed in tty mode (Close: 3980)Gravatar Enrico Tassi2015-02-05
| | | | Here nonsensical means a Qed/Defined without a Lemma.
* Windows installer cleanupGravatar Enrico Tassi2015-02-05
|
* Marshal.from_string on 32 bit systems use tmpfile if needed (Close: 3968)Gravatar Enrico Tassi2015-02-05
| | | | | | | | 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).
* Properly set module names in presence of -Q. (Fix for bug #3958)Gravatar Guillaume Melquiond2015-02-05
| | | | | | | | 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.
* Detecting automatically whether .opt versions of ocaml executables exist;Gravatar Hugo Herbelin2015-02-04
| | | | making configure option -opt deprecated.
* Optimized Import/Export the same way as Require Import/Export wasGravatar Hugo Herbelin2015-02-04
| | | | | | 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).
* Fixing bug #3996.Gravatar Pierre-Marie Pédrot2015-02-04
|
* More efficient implementation of Richpp.Gravatar Pierre-Marie Pédrot2015-02-04
| | | | | Instead of constructing the XML string and parsing it afterwards, we build it by hijacking the formatting output.
* Tactic Notation: use stable unique key for notations (Close: 3970)Gravatar Enrico Tassi2015-02-04
|
* CThread: workaround for threads lockup on windwos made more aggressiveGravatar Enrico Tassi2015-02-04
|
* Nativelib: catch Unix_error (like no ocamlopt found)Gravatar Enrico Tassi2015-02-04
|
* Revert "Tactic Notation: use stable unique key for notations (Close: 3970)"Gravatar Enrico Tassi2015-02-03
| | | | This reverts commit 2e09a22baeb93c57e6d8388313dc638349679910.
* Tactic Notation: use stable unique key for notations (Close: 3970)Gravatar Enrico Tassi2015-02-03
|
* spit module path using / as directory separatorGravatar Enrico Tassi2015-02-03
| | | | | | | | 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.
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
|
* Fix index of reference manual.Gravatar Guillaume Melquiond2015-01-29
|
* An update on INSTALL.ide.Gravatar Hugo Herbelin2015-01-29
|
* Removing outdated INSTALL.macosx file; instructions are more likely toGravatar Hugo Herbelin2015-01-29
| | | | | | be up-to-date on the web. If someone can check that INSTALL.win is up-to-date, that'd be nice.
* Extra check at the INSTALL file.Gravatar Hugo Herbelin2015-01-29
|
* Remove spurious "Loading ML file" and "<W> Grammar extension" from the ↵Gravatar Guillaume Melquiond2015-01-29
| | | | reference manual.
* Remove some "Warning:" from the reference manual.Gravatar Guillaume Melquiond2015-01-29
|
* Prevent spurious warnings about Arguments.Gravatar Guillaume Melquiond2015-01-29
| | | | | | | | | | | | | 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.
* Made the CoqIDE progress gutter clickable.Gravatar Pierre-Marie Pédrot2015-01-29
|
* Fix some typos in the documentation.Gravatar Guillaume Melquiond2015-01-29
|
* Fix some broken Coq scripts in the reference manual.Gravatar Guillaume Melquiond2015-01-29
|
* Fixing bug #3931.Gravatar Pierre-Marie Pédrot2015-01-28
|
* Fixed a wrong warning in coq_makefile.Gravatar Pierre Courtieu2015-01-27
| | | | A non empty dir detected as an empty one.
* Allow -type-in-type to be an option also for coqc.Gravatar Daniel R. Grayson2015-01-27
|
* Doc: Overfull lines in chapter on Canonical Structures.Gravatar Hugo Herbelin2015-01-27
|
* Made replacing of text in CoqIDE atomic w.r.t. the undo/redo.Gravatar Pierre-Marie Pédrot2015-01-25
|
* Fixing bug #3947.Gravatar Pierre-Marie Pédrot2015-01-25
|
* Test for bug #3798.Gravatar Pierre-Marie Pédrot2015-01-25
|
* Doc: Fixing some compilation problems with chapter CanonicalGravatar Hugo Herbelin2015-01-24
| | | | | Structures. Text mode + a "Require Import" in a module which provokes suspect warnings "Exception Not_found".
* Updating CHANGES (grammar, thanks to AS for pointing it out) +Gravatar Hugo Herbelin2015-01-24
| | | | a line on "Intuition Negation Unfolding".
* Removed obsolete option "Legacy Partially Applied EliminationGravatar Hugo Herbelin2015-01-24
| | | | | | | 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).
* Reference Manual: Documenting new printing of evars and new effect ofGravatar Hugo Herbelin2015-01-24
| | | | Set Printing Existential Instances (see bug report #3951).
* Equality Schemes options: reverting commit ff9f94634 which isGravatar Hugo Herbelin2015-01-24
| | | | | | | 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.
* Isolate a function for printing evar sets.Gravatar Hugo Herbelin2015-01-24
|
* Tentative workaround for bug #3798.Gravatar Pierre-Marie Pédrot2015-01-24
| | | | Ultimately setoid rewrite should be written in the monad to fix it properly.
* Fix previous commit on extraction.Gravatar Maxime Dénès2015-01-23
| | | | | Since name clashes are discovered by side effects, the order of traversal of module structs cannot be changed.
* Typos, grammar, layout in CHANGES (continued).Gravatar Hugo Herbelin2015-01-23
|
* Typos, grammar, layout in CHANGES.Gravatar Hugo Herbelin2015-01-23
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 12:07:16 +0000