| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-11-06 | Fixed #4407. | Pierre Courtieu | |
| Like coqc: detect if the current directory was set by options, if not: add it with empty logical path. TODO: check if coq_makefile is still correct wrt to this modification, I think yes, actually it should end being more correct. | |||
| 2015-11-06 | Fixing #4406 coqdep: No recursive search of ml (-I). | Pierre Courtieu | |
| 2015-10-23 | Support "Functional Scheme" in coqdoc. (Fix bug #4382) | Guillaume Melquiond | |
| 2015-09-26 | Documenting how to support some special unicode characters in coqdoc | Hugo Herbelin | |
| (thanks to coq-club, Sep 2015). | |||
| 2015-09-26 | Clarifying the doc of coqdoc --utf8 as discussed on coq-club on August 19, 2015. | Hugo Herbelin | |
| 2015-09-25 | Updating the documentation and the toolchain w.r.t. the change in -compile. | Pierre-Marie Pédrot | |
| 2015-09-16 | Change coq_makefile's default from "-Q . Top" to "-R . Top". (Fix bug #3603) | Guillaume Melquiond | |
| 2015-09-03 | Missing argument "-c" for coqdep in coq_makefile | mlasson | |
| Prior to commit 964d1b70, the dependency files .mllib.d and .mlpack.d were generated by a call to coqdep using the argument -c (for ocaml code). While doing some finetuning of the generation of implicit rules, this commit removed (I think by mistake) this "-c". And without this -c argument coqdep output nothing on mllib files leading to incorrect linking of mllibs. | |||
| 2015-08-13 | report the full module path when reporting errors in coqdep | Gregory Malecha | |
| 2015-07-31 | Remove some outdated files and fix permissions. | Guillaume Melquiond | |
| 2015-07-30 | Fix width of underscore in coq_tex output. | Guillaume Melquiond | |
| 2015-07-30 | Fix broken regexp. | Guillaume Melquiond | |
| Characters do not need to be escaped in character ranges. It just had the effect of matching backslashes four times. | |||
| 2015-07-30 | Remove unused variables. | Guillaume Melquiond | |
| 2015-07-30 | Remove usage of Printexc.catch in the tools, as it is deprecated since 2001. | Guillaume Melquiond | |
| "This function is deprecated: the runtime system is now able to print uncaught exceptions as precisely as Printexc.catch does. Moreover, calling Printexc.catch makes it harder to track the location of the exception using the debugger or the stack backtrace facility. So, do not use Printexc.catch in new code." | |||
| 2015-07-29 | Make coq-tex more robust with respect to the (non-)command on the last line. | Guillaume Melquiond | |
| 2015-07-29 | Remove empty commands from the output of coq-tex. | Guillaume Melquiond | |
| 2015-07-29 | Rewrite the main loop of coq-tex. | Guillaume Melquiond | |
| Before this commit, coq-tex was reading the .v file and was guessing how many lines from the coqtop output it should display. Now, it reads the coqtop output and it guesses how many lines from the .v file it should display. That way, coq-tex no longer needs to embed a parser; it relies on coqtop for parsing. This is much more robust and makes it possible to properly handle script such as the following one: Goal { True } + { False }. { left. exact I. } As before, if there is a way for a script to produce something that looks like a prompt (that is, a line that starts with "foo < "), coq-tex will be badly confused. | |||
| 2015-07-28 | Make coq-tex aware of lines ending with "}", so as to fix the FAQ. | Guillaume Melquiond | |
| This is only a heuristic and it might cause the tool to become awfully confused if a line ends with "}" yet this is not the end of a tactic block. Fixing it would require a full-blown Coq parser inside coq-tex. Example of crazy output: Coq < Goal { True } Coq < 1 subgoal ============================ {True} + {False} Coq < + { False }. | |||
| 2015-07-24 | Using maps and sets instead of lists in coqdep. | Pierre-Marie Pédrot | |
| 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. | |||
| 2015-07-24 | Fixing bug #4265: "coqdep does not handle From ... Require" for good. | Pierre-Marie Pédrot | |
| 2015-07-08 | Fix command-line documentation of coq-tex. | Guillaume Melquiond | |
| 2015-07-03 | Fixing bug #4265: coqdep does not handle From ... Require. | Pierre-Marie Pédrot | |
| 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. | |||
| 2015-06-30 | Removing dead code in coqdep. | Pierre-Marie Pédrot | |
| 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. | |||
| 2015-06-09 | Support CRLF end of line in fake_ide. | Guillaume Melquiond | |
| 2015-05-28 | Test for 4159 | Enrico Tassi | |
| 2015-05-18 | Adding the -color option to coqc. | Pierre Courtieu | |
| 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. | |||
| 2015-05-14 | Do not regenerate .d files when cleaning them. (Fix bug #4079) | Guillaume Melquiond | |
| 2015-05-14 | Adding an option -w to control Coq warning output. | Pierre-Marie Pédrot | |
| 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. | |||
| 2015-05-14 | Disable precompilation for native_compute by default. | Guillaume Melquiond | |
| 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. | |||
| 2015-04-22 | Remove some spurious spaces in generated Makefiles. | Guillaume Melquiond | |
| 2015-04-20 | Remove spurious ".v" from warning message. | Guillaume Melquiond | |
| 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 | coq_makefile: fix compilation with camlp4 | Enrico Tassi | |
| 2015-03-27 | Properly handle extra "clean" targets with coq_makefile. | Guillaume Melquiond | |
| 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-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-27 | Make coq_makefile generate double-colon rules for clean and archclean. (Fix ↵ | Guillaume Melquiond | |
| bug #4080) | |||
| 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-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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |