aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
Commit message (Collapse)AuthorAge
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-30
|\
| * use printf instead of sequenced calls to print.Gravatar Gregory Malecha2016-03-24
| |
| * add a .merlin target to the makefileGravatar Gregory Malecha2016-03-24
| |
* | Creating a dedicated ltac/ folder for Hightactics.Gravatar Pierre-Marie Pédrot2016-03-21
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\|
| * Tentative fix for bug #4522: Incorrect "Warning..." on windows.Gravatar Pierre-Marie Pédrot2016-01-24
| |
| * Fixing bug #4373: coqdep does not know about .vio files.Gravatar Pierre-Marie Pédrot2016-01-24
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
| * Minor edits in output of coqdep --help.Gravatar Maxime Dénès2016-01-15
| |
| * Fix #4408.Gravatar Pierre Courtieu2016-01-15
| | | | | | | | | | Removed documentation for broken -D -w (but the option are still there). Fixed documentation of others.
| * Partially fixing #4408: coqdep --help is up to date.Gravatar Pierre Courtieu2016-01-15
| |
* | Remove deprecated command-line options such as "-as".Gravatar Guillaume Melquiond2016-01-06
| |
* | Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Guillaume Melquiond2016-01-06
|\| | | | | | | | | Conflicts: lib/cSig.mli
| * Disable warning 31 when generating coqtop from coqmktop.Gravatar Maxime Dénès2016-01-05
| | | | | | | | | | | | | | | | | | | | | | | | | | In OCaml 3.x, the toploop of OCaml was accessible from toplevellib.cma. In OCaml 4.x, it was replaced by compiler-libs. However, linking with compiler-libs produces a warning (fatal with OCaml 4.03) as soon as we have a file named errors.ml or lexer.ml... The only satisfactory solution seems to be to "pack" compiler libs. But it is not done currently in the OCaml distribution, and implementing it in coqmktop at this point would be too risky. So for now, I am disabling the warning until we hear from the OCaml team. In principle, this clash of modules names can break OCaml's type safety, so we are living dangerously.
* | Remove unused functions.Gravatar Guillaume Melquiond2016-01-01
| |
* | Remove useless recursive flags.Gravatar Guillaume Melquiond2016-01-01
| |
* | Remove some occurrences of Unix.opendir.Gravatar Guillaume Melquiond2015-12-14
| |
* | Simplify coqdep lexer by removing global references.Gravatar Guillaume Melquiond2015-11-30
| |
* | Merge remote-tracking branch 'origin/v8.5' into upstream-trunkGravatar Hugo Herbelin2015-11-07
|\| | | | | | | | | - Had to add a Sigma.to_evar_map - Had to rework coqdep_common.ml{,i} and coqdep.ml
| * Fixed #4407.Gravatar Pierre Courtieu2015-11-06
| | | | | | | | | | | | | | 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.
| * Fixing #4406 coqdep: No recursive search of ml (-I).Gravatar Pierre Courtieu2015-11-06
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-26
|\|
| * Support "Functional Scheme" in coqdoc. (Fix bug #4382)Gravatar Guillaume Melquiond2015-10-23
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\|
| * Documenting how to support some special unicode characters in coqdocGravatar Hugo Herbelin2015-09-26
| | | | | | | | (thanks to coq-club, Sep 2015).
| * Clarifying the doc of coqdoc --utf8 as discussed on coq-club on August 19, 2015.Gravatar Hugo Herbelin2015-09-26
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-09-25
|\|
| * Updating the documentation and the toolchain w.r.t. the change in -compile.Gravatar Pierre-Marie Pédrot2015-09-25
| |
* | Fixing fake_ide.Gravatar Pierre-Marie Pédrot2015-09-22
| |
* | Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-09-17
|\|
| * Change coq_makefile's default from "-Q . Top" to "-R . Top". (Fix bug #3603)Gravatar Guillaume Melquiond2015-09-16
| |
* | Coq_makefile: read TIMED and TIMECMD from environment.Gravatar Maxime Dénès2015-09-13
| | | | | | | | Useful e.g. with submakefiles.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-09-06
|\|
| * Missing argument "-c" for coqdep in coq_makefileGravatar mlasson2015-09-03
| | | | | | | | | | | | | | | | | | 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.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-08-22
|\|
| * report the full module path when reporting errors in coqdepGravatar Gregory Malecha2015-08-13
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-08-05
|\|
| * Remove some outdated files and fix permissions.Gravatar Guillaume Melquiond2015-07-31
| |
| * Fix width of underscore in coq_tex output.Gravatar Guillaume Melquiond2015-07-30
| |
| * Fix broken regexp.Gravatar Guillaume Melquiond2015-07-30
| | | | | | | | | | Characters do not need to be escaped in character ranges. It just had the effect of matching backslashes four times.
| * Remove unused variables.Gravatar Guillaume Melquiond2015-07-30
| |
| * Remove usage of Printexc.catch in the tools, as it is deprecated since 2001.Gravatar Guillaume Melquiond2015-07-30
| | | | | | | | | | | | | | | | "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."
| * Make coq-tex more robust with respect to the (non-)command on the last line.Gravatar Guillaume Melquiond2015-07-29
| |
| * Remove empty commands from the output of coq-tex.Gravatar Guillaume Melquiond2015-07-29
| |
| * Rewrite the main loop of coq-tex.Gravatar Guillaume Melquiond2015-07-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-07-29
|\|
| * Make coq-tex aware of lines ending with "}", so as to fix the FAQ.Gravatar Guillaume Melquiond2015-07-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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 }.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-07-27
|\|
| * Using maps and sets instead of lists in coqdep.Gravatar Pierre-Marie Pédrot2015-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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-09 15:19:49 +0000