| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-04-02 | Avoid outputting stray "Local" keywords in HTML documentation. | Guillaume Melquiond | |
| 2015-03-31 | Do not escape "'" when outputting to html, especially not using "´". | Guillaume Melquiond | |
| 2015-03-30 | Merge branch 'v8.5' into trunk | Enrico Tassi | |
| 2015-03-30 | coq_makefile: fix compilation with camlp4 | Enrico Tassi | |
| 2015-03-27 | Properly handle extra "clean" targets with coq_makefile. | Guillaume Melquiond | |
| 2015-03-23 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-03-14 | End of Bug 3986 - make cleanall removes .*.aux files | Pierre Boutillier | |
| 2015-03-14 | Bug 3981 ends to convice me that subdirs in coq_makefile deverse a warning | Pierre Boutillier | |
| 2015-03-04 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-28 | Coq_makefile clean target erases .coq-native dirs in . if they are empty | Pierre Boutillier | |
| 2015-02-28 | Fixing the rule for ml4 depencies in coq_makefile | mlasson | |
| 2015-02-28 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-27 | Make coq_makefile generate double-colon rules for clean and archclean. (Fix ↵ | Guillaume Melquiond | |
| bug #4080) | |||
| 2015-02-27 | Adding a new folder corresponding to the low-level part of the pretyper | Pierre-Marie Pédrot | |
| 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. | |||
| 2015-02-26 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-26 | Fixing printing error in coq_makefile. | Pierre-Marie Pédrot | |
| 2015-02-26 | Mention -R option in warnings, fixing #4067 and #4068. | Maxime Dénès | |
| 2015-02-24 | Update the list of phony targets produced by coq_makefile. (Fix for bug #4084) | Guillaume Melquiond | |
| Also make uninstall_me.sh a real target with proper dependencies. | |||
| 2015-02-16 | Using same code for browsing physical directories in coqtop and coqdep. | Hugo Herbelin | |
| 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. | |||
| 2015-02-16 | Using home-made ocamllibdep rather than coqdep_boot. | Hugo Herbelin | |
| 2015-02-16 | New short stand-alone ocamllibdep to build .mllib dependencies files. | Hugo Herbelin | |
| 2015-02-16 | Restricting the need for coqdep_boot to mllib.d files (since ocaml | Hugo Herbelin | |
| 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). | |||
| 2015-02-14 | coqc accepts -top option. Fixes bug #4043. | Pierre-Marie Pédrot | |
| 2015-02-12 | Revert "Using same code for browsing physical directories in coqtop and coqdep." | Hugo Herbelin | |
| (Sorry, was not intended to be pushed) This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c. | |||
| 2015-02-12 | Revert "Capital letter in plugins." (Sorry, was not intended to be pushed) | Hugo Herbelin | |
| This reverts commit bff2b36cb0e2dbd02c4f181fba545a420e847767. | |||
| 2015-02-12 | Capital letter in plugins. | Hugo Herbelin | |
| 2015-02-12 | Using same code for browsing physical directories in coqtop and coqdep. | Hugo Herbelin | |
| 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). | |||
| 2015-02-11 | Make coqdoc -l properly handle Local before Ltac. (Fix for bug #3307) | Guillaume Melquiond | |
| 2015-02-10 | Prevent Latex from messing with backticks. (Fix for bug #3871) | Guillaume Melquiond | |
| 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-16 | coq_makefile: install also .v and .glob | Enrico Tassi | |
| 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 | |||
| 2015-01-15 | Remove left-over dead code in previous commit. | Maxime Dénès | |
| 2015-01-15 | Make -print-mod-uid accept a list of files. | Maxime Dénès | |
| Solves an efficiency problem in Makefiles generated by coq_makefile. | |||
| 2015-01-15 | Make installation of native files more robust. | Maxime Dénès | |
| 2015-01-15 | coq_makefile installs native files | Pierre Boutillier | |
| 2015-01-14 | coq_makefile: chmod 755 on toplopp cmxs | Enrico Tassi | |
| 2015-01-13 | Made -print-mod-uid more silent and robust. | Maxime Dénès | |
| This is a follow-up on Pierre's 5d80a385. | |||
| 2015-01-12 | Coq_makefile erases native compiler files | Pierre Boutillier | |
| 2015-01-12 | Update headers. | Maxime Dénès | |
| 2015-01-12 | Fixing typo in previous commit. | Hugo Herbelin | |
| 2015-01-11 | Fixing wrong duplication message when finding both a .ml and a .ml4 in coqdep. | Hugo Herbelin | |
| 2015-01-06 | rename: vi -> vio | Enrico Tassi | |
| 2015-01-06 | Improve error recovery in case of ill-formed coqdoc comment. (Fix for bug ↵ | Guillaume Melquiond | |
| #3802.) | |||
| 2014-12-25 | Inlining Spawn.kill_if in the one place were it was actually used, thus | Pierre-Marie Pédrot | |
| removing the need of thread creation in the interface. | |||
| 2014-12-18 | Bug fix (coq_makefile): Adding unix.cma and threads.cma dependencies for ↵ | mlasson | |
| grammar in campl4 | |||
| 2014-12-15 | Fixing bug #3865. | Pierre-Marie Pédrot | |
| 2014-12-12 | Fix #3800 : cmxs need execution priviledges under windows | Pierre Boutillier | |
| 2014-12-09 | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey | |
| 2014-12-09 | coqdoc.css: fix a few errors | Pierre Letouzey | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |