Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Support CRLF end of line in fake_ide. | 2015-06-09 | |
| | |||
* | Test for 4159 | 2015-05-28 | |
| | |||
* | Adding the -color option to coqc. | 2015-05-18 | |
| | | | | | | coqc by default uses colors, this allows to disable it. Moreover, colors are not yet correctly disabled when compiling from emacs (emacs bugs?), making this option even more useful. | ||
* | Do not regenerate .d files when cleaning them. (Fix bug #4079) | 2015-05-14 | |
| | |||
* | Adding an option -w to control Coq warning output. | 2015-05-14 | |
| | | | | | | | For now, warnings are still ignored by default, but this may change. This commit at least allows to print them whenever desired. The -w syntax is also opened to future additions to further control the display of warnings. | ||
* | Disable precompilation for native_compute by default. | 2015-05-14 | |
| | | | | | | | | | | | | | | Note that this does not prevent using native_compute, but it will force on-the-fly recompilation of dependencies whenever it is used. Precompilation is enabled for the standard library, assuming native compilation was enabled at configuration time. If native compilation was disabled at configuration time, native_compute falls back to vm_compute. Failure to precompile is a hard error, since it is now explicitly required by the user. | ||
* | Remove some spurious spaces in generated Makefiles. | 2015-04-22 | |
| | |||
* | Remove spurious ".v" from warning message. | 2015-04-20 | |
| | |||
* | Avoid outputting stray "Local" keywords in HTML documentation. | 2015-04-02 | |
| | |||
* | Do not escape "'" when outputting to html, especially not using "´". | 2015-03-31 | |
| | |||
* | coq_makefile: fix compilation with camlp4 | 2015-03-30 | |
| | |||
* | Properly handle extra "clean" targets with coq_makefile. | 2015-03-27 | |
| | |||
* | End of Bug 3986 - make cleanall removes .*.aux files | 2015-03-14 | |
| | |||
* | Bug 3981 ends to convice me that subdirs in coq_makefile deverse a warning | 2015-03-14 | |
| | |||
* | Coq_makefile clean target erases .coq-native dirs in . if they are empty | 2015-02-28 | |
| | |||
* | Fixing the rule for ml4 depencies in coq_makefile | 2015-02-28 | |
| | |||
* | Make coq_makefile generate double-colon rules for clean and archclean. (Fix ↵ | 2015-02-27 | |
| | | | | bug #4080) | ||
* | Fixing printing error in coq_makefile. | 2015-02-26 | |
| | |||
* | Mention -R option in warnings, fixing #4067 and #4068. | 2015-02-26 | |
| | |||
* | Update the list of phony targets produced by coq_makefile. (Fix for bug #4084) | 2015-02-24 | |
| | | | | Also make uninstall_me.sh a real target with proper dependencies. | ||
* | coqc accepts -top option. Fixes bug #4043. | 2015-02-14 | |
| | |||
* | Revert "Using same code for browsing physical directories in coqtop and coqdep." | 2015-02-12 | |
| | | | | | | (Sorry, was not intended to be pushed) This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c. | ||
* | Revert "Capital letter in plugins." (Sorry, was not intended to be pushed) | 2015-02-12 | |
| | | | | This reverts commit bff2b36cb0e2dbd02c4f181fba545a420e847767. | ||
* | Capital letter in plugins. | 2015-02-12 | |
| | |||
* | Using same code for browsing physical directories in coqtop and coqdep. | 2015-02-12 | |
| | | | | | | | 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). | ||
* | Make coqdoc -l properly handle Local before Ltac. (Fix for bug #3307) | 2015-02-11 | |
| | |||
* | Prevent Latex from messing with backticks. (Fix for bug #3871) | 2015-02-10 | |
| | |||
* | Fixed a wrong warning in coq_makefile. | 2015-01-27 | |
| | | | | A non empty dir detected as an empty one. | ||
* | Allow -type-in-type to be an option also for coqc. | 2015-01-27 | |
| | |||
* | coq_makefile: install also .v and .glob | 2015-01-16 | |
| | | | | | | This is useful for PIDE based interfaces, since they can build hyperlinks out of .glob files and let the user jump to the corresponding .v files | ||
* | Remove left-over dead code in previous commit. | 2015-01-15 | |
| | |||
* | Make -print-mod-uid accept a list of files. | 2015-01-15 | |
| | | | | Solves an efficiency problem in Makefiles generated by coq_makefile. | ||
* | Make installation of native files more robust. | 2015-01-15 | |
| | |||
* | coq_makefile installs native files | 2015-01-15 | |
| | |||
* | coq_makefile: chmod 755 on toplopp cmxs | 2015-01-14 | |
| | |||
* | Made -print-mod-uid more silent and robust. | 2015-01-13 | |
| | | | | This is a follow-up on Pierre's 5d80a385. | ||
* | Coq_makefile erases native compiler files | 2015-01-12 | |
| | |||
* | Update headers. | 2015-01-12 | |
| | |||
* | Fixing typo in previous commit. | 2015-01-12 | |
| | |||
* | Fixing wrong duplication message when finding both a .ml and a .ml4 in coqdep. | 2015-01-11 | |
| | |||
* | rename: vi -> vio | 2015-01-06 | |
| | |||
* | Improve error recovery in case of ill-formed coqdoc comment. (Fix for bug ↵ | 2015-01-06 | |
| | | | | #3802.) | ||
* | Inlining Spawn.kill_if in the one place were it was actually used, thus | 2014-12-25 | |
| | | | | removing the need of thread creation in the interface. | ||
* | Bug fix (coq_makefile): Adding unix.cma and threads.cma dependencies for ↵ | 2014-12-18 | |
| | | | | grammar in campl4 | ||
* | Fixing bug #3865. | 2014-12-15 | |
| | |||
* | Fix #3800 : cmxs need execution priviledges under windows | 2014-12-12 | |
| | |||
* | Switch the few remaining iso-latin-1 files to utf8 | 2014-12-09 | |
| | |||
* | coqdoc.css: fix a few errors | 2014-12-09 | |
| | |||
* | coqdoc: fix a few issues with xhtml validity (backport 1636f7 and 754abf1 ↵ | 2014-12-09 | |
| | | | | | | | | | | | | | | | | | from v8.4) - For the style of identifiers, coqdoc was using a 'type' attribute of tag <span>. But this attribute isn't a legal attribute of tag <span> according to the xhtml norm. Instead, I propose to use 'title' for that. The coqdoc.css now supports both approaches. - The names of inner links (cross references #foo) were containing arbitrary characters (in the case of a notation string). For instance in Utf8_core : <a name=":type_scope:'∀'_x_'..'_x_','_x"> Instead, when strange characters are detected, we now hash the string via Digest, and use this hexa hash as html label. - And some whitespace before /> | ||
* | Port to trunk commit r16062 of v8.4 (Correction des entêtes pour la ↵ | 2014-12-09 | |
| | | | | documentation en ligne) |