| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-09-25 | Updating the documentation and the toolchain w.r.t. the change in -compile. | Pierre-Marie Pédrot | |
| 2015-09-22 | Fixing fake_ide. | Pierre-Marie Pédrot | |
| 2015-09-17 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 2015-09-16 | Change coq_makefile's default from "-Q . Top" to "-R . Top". (Fix bug #3603) | Guillaume Melquiond | |
| 2015-09-13 | Coq_makefile: read TIMED and TIMECMD from environment. | Maxime Dénès | |
| Useful e.g. with submakefiles. | |||
| 2015-09-06 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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-22 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-08-13 | report the full module path when reporting errors in coqdep | Gregory Malecha | |
| 2015-08-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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-27 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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-18 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-07-08 | Fix command-line documentation of coq-tex. | Guillaume Melquiond | |
| 2015-07-06 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 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-07-02 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 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-22 | Merge remote-tracking branch 'forge/v8.5' | Pierre Boutillier | |
| 2015-06-22 | All invocations to ocaml compilers go through ocamlfind | Pierre Boutillier | |
| Nothing is done for camlp4 There is an issue with computing camlbindir | |||
| 2015-06-09 | Support CRLF end of line in fake_ide. | Guillaume Melquiond | |
| 2015-06-01 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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-15 | Merge v8.5 into trunk | Hugo Herbelin | |
| Conflicts: tactics/eauto.ml4 (merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API) | |||
| 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-05-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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-09 | Merge branch 'v8.5' into trunk | Pierre Letouzey | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |