Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| * | Using maps and sets instead of lists in coqdep. | 2015-07-24 | ||
| | | | | | | | | | | | | The quadratic behaviour of list searching probably appears with small enough samples. With the advent of usable libraries in Coq, and thus many possible dependencies, better be safe than sorry. | |||
| * | Fixing bug #4265: "coqdep does not handle From ... Require" for good. | 2015-07-24 | ||
| | | ||||
* | | Merge branch 'v8.5' | 2015-07-18 | ||
|\| | ||||
| * | Fix command-line documentation of coq-tex. | 2015-07-08 | ||
| | | ||||
* | | Merge branch 'v8.5' into trunk | 2015-07-06 | ||
|\| | ||||
| * | Fixing bug #4265: coqdep does not handle From ... Require. | 2015-07-03 | ||
| | | | | | | | | | | | | The search algorithm is not satisfactory though, as it crawls through all known files to find the proper one. We should rather use some trie-based data structure, but I'll leave this for a future commit. | |||
* | | Merge branch 'v8.5' into trunk | 2015-07-02 | ||
|\| | ||||
| * | Removing dead code in coqdep. | 2015-06-30 | ||
| | | | | | | | | | | | | Since commit 2f521670fbd, the Require "file" syntax was not used anymore by coqtop but the code handling it was still there in coqdep. We finish the work by erasing the remnant code. | |||
* | | Merge remote-tracking branch 'forge/v8.5' | 2015-06-22 | ||
|\| | ||||
* | | All invocations to ocaml compilers go through ocamlfind | 2015-06-22 | ||
| | | | | | | | | | | Nothing is done for camlp4 There is an issue with computing camlbindir | |||
| * | Support CRLF end of line in fake_ide. | 2015-06-09 | ||
| | | ||||
* | | Merge branch 'v8.5' | 2015-06-01 | ||
|\| | ||||
| * | 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. | |||
* | | Merge v8.5 into trunk | 2015-05-15 | ||
|\| | | | | | | | | | | | | | Conflicts: tactics/eauto.ml4 (merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API) | |||
| * | 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. | |||
* | | Merge branch 'v8.5' | 2015-05-05 | ||
|\| | ||||
| * | Remove some spurious spaces in generated Makefiles. | 2015-04-22 | ||
| | | ||||
| * | Remove spurious ".v" from warning message. | 2015-04-20 | ||
| | | ||||
* | | Merge branch 'v8.5' into trunk | 2015-04-09 | ||
|\| | ||||
| * | Avoid outputting stray "Local" keywords in HTML documentation. | 2015-04-02 | ||
| | | ||||
| * | Do not escape "'" when outputting to html, especially not using "´". | 2015-03-31 | ||
| | | ||||
* | | Merge branch 'v8.5' into trunk | 2015-03-30 | ||
|\| | ||||
| * | coq_makefile: fix compilation with camlp4 | 2015-03-30 | ||
| | | ||||
| * | Properly handle extra "clean" targets with coq_makefile. | 2015-03-27 | ||
| | | ||||
* | | Merge branch 'v8.5' | 2015-03-23 | ||
|\| | ||||
| * | 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 | ||
| | | ||||
* | | Merge branch 'v8.5' | 2015-03-04 | ||
|\| | ||||
| * | 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 | ||
| | | ||||
* | | Merge branch 'v8.5' | 2015-02-28 | ||
|\| | ||||
| * | Make coq_makefile generate double-colon rules for clean and archclean. (Fix ↵ | 2015-02-27 | ||
| | | | | | | | | bug #4080) | |||
* | | Adding a new folder corresponding to the low-level part of the pretyper | 2015-02-27 | ||
| | | | | | | | | | | | | | | together with the tactic monad. The move is not complete yet, because some file candidates for this directory have almost useless dependencies in other ones that should not be moved. | |||
* | | Merge branch 'v8.5' | 2015-02-26 | ||
|\| | ||||
| * | 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. | |||
* | | Using same code for browsing physical directories in coqtop and coqdep. | 2015-02-16 | ||
| | | | | | | | | | | | | | | | | 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), - uniformly expecting paths in Unix format and warning otherwise. | |||
* | | Using home-made ocamllibdep rather than coqdep_boot. | 2015-02-16 | ||
| | | ||||
* | | New short stand-alone ocamllibdep to build .mllib dependencies files. | 2015-02-16 | ||
| | | ||||
* | | Restricting the need for coqdep_boot to mllib.d files (since ocaml | 2015-02-16 | ||
|/ | | | | | 3.12.1, ocamldep was able to deal with .ml4, so that building .mllib.d is the only feature that coqdep_boot was still required for). | |||
* | 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 | ||
| |