aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
Commit message (Collapse)AuthorAge
* Coq_makefile clean target erases .coq-native dirs in . if they are emptyGravatar Pierre Boutillier2015-02-28
|
* Fixing the rule for ml4 depencies in coq_makefileGravatar mlasson2015-02-28
|
* Make coq_makefile generate double-colon rules for clean and archclean. (Fix ↵Gravatar Guillaume Melquiond2015-02-27
| | | | bug #4080)
* Fixing printing error in coq_makefile.Gravatar Pierre-Marie Pédrot2015-02-26
|
* Mention -R option in warnings, fixing #4067 and #4068.Gravatar Maxime Dénès2015-02-26
|
* Update the list of phony targets produced by coq_makefile. (Fix for bug #4084)Gravatar Guillaume Melquiond2015-02-24
| | | | Also make uninstall_me.sh a real target with proper dependencies.
* coqc accepts -top option. Fixes bug #4043.Gravatar Pierre-Marie Pédrot2015-02-14
|
* Revert "Using same code for browsing physical directories in coqtop and coqdep."Gravatar Hugo Herbelin2015-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)Gravatar Hugo Herbelin2015-02-12
| | | | This reverts commit bff2b36cb0e2dbd02c4f181fba545a420e847767.
* Capital letter in plugins.Gravatar Hugo Herbelin2015-02-12
|
* Using same code for browsing physical directories in coqtop and coqdep.Gravatar Hugo Herbelin2015-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)Gravatar Guillaume Melquiond2015-02-11
|
* Prevent Latex from messing with backticks. (Fix for bug #3871)Gravatar Guillaume Melquiond2015-02-10
|
* Fixed a wrong warning in coq_makefile.Gravatar Pierre Courtieu2015-01-27
| | | | A non empty dir detected as an empty one.
* Allow -type-in-type to be an option also for coqc.Gravatar Daniel R. Grayson2015-01-27
|
* coq_makefile: install also .v and .globGravatar Enrico Tassi2015-01-16
| | | | | | 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
* Remove left-over dead code in previous commit.Gravatar Maxime Dénès2015-01-15
|
* Make -print-mod-uid accept a list of files.Gravatar Maxime Dénès2015-01-15
| | | | Solves an efficiency problem in Makefiles generated by coq_makefile.
* Make installation of native files more robust.Gravatar Maxime Dénès2015-01-15
|
* coq_makefile installs native filesGravatar Pierre Boutillier2015-01-15
|
* coq_makefile: chmod 755 on toplopp cmxsGravatar Enrico Tassi2015-01-14
|
* Made -print-mod-uid more silent and robust.Gravatar Maxime Dénès2015-01-13
| | | | This is a follow-up on Pierre's 5d80a385.
* Coq_makefile erases native compiler filesGravatar Pierre Boutillier2015-01-12
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Fixing typo in previous commit.Gravatar Hugo Herbelin2015-01-12
|
* Fixing wrong duplication message when finding both a .ml and a .ml4 in coqdep.Gravatar Hugo Herbelin2015-01-11
|
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
|
* Improve error recovery in case of ill-formed coqdoc comment. (Fix for bug ↵Gravatar Guillaume Melquiond2015-01-06
| | | | #3802.)
* Inlining Spawn.kill_if in the one place were it was actually used, thusGravatar Pierre-Marie Pédrot2014-12-25
| | | | removing the need of thread creation in the interface.
* Bug fix (coq_makefile): Adding unix.cma and threads.cma dependencies for ↵Gravatar mlasson2014-12-18
| | | | grammar in campl4
* Fixing bug #3865.Gravatar Pierre-Marie Pédrot2014-12-15
|
* Fix #3800 : cmxs need execution priviledges under windowsGravatar Pierre Boutillier2014-12-12
|
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
|
* coqdoc.css: fix a few errorsGravatar Pierre Letouzey2014-12-09
|
* coqdoc: fix a few issues with xhtml validity (backport 1636f7 and 754abf1 ↵Gravatar Pierre Letouzey2014-12-09
| | | | | | | | | | | | | | | | | from v8.4) - For the style of identifiers, coqdoc was using a 'type' attribute of tag <span>. But this attribute isn't a legal attribute of tag <span> according to the xhtml norm. Instead, I propose to use 'title' for that. The coqdoc.css now supports both approaches. - The names of inner links (cross references #foo) were containing arbitrary characters (in the case of a notation string). For instance in Utf8_core : <a name=":type_scope:'∀'_x_'..'_x_','_x"> Instead, when strange characters are detected, we now hash the string via Digest, and use this hexa hash as html label. - And some whitespace before />
* Port to trunk commit r16062 of v8.4 (Correction des entêtes pour la ↵Gravatar notin2014-12-09
| | | | documentation en ligne)
* coqdep: granting #2506 (./dir is the same as dir)Gravatar Hugo Herbelin2014-12-04
|
* coqdep: Warning about ml file clashes, keeping the file correspondingGravatar Hugo Herbelin2014-12-04
| | | | | | | | to the first -I option. Fortunately, with -I option, only one file can be found by occurrence of the option, so on the contrary of -Q/-R options for v files, the order is not file-system dependent.
* Use the url package, since coqdoc generates \url commands.Gravatar Guillaume Melquiond2014-10-27
|
* Supporting Greek and Coptic (U0370) as first letter of coqdoc identifiers.Gravatar Hugo Herbelin2014-10-22
|
* More fallout from elisp renameGravatar Anders Kaseorg2014-10-16
| | | | | | | | | | Commit 3e972b3ff8e532be233f70567c87512324c99b4e renamed coq.el, coq-db.el, coq-syntax.el to gallina.el, gallina-db.el, gallina-syntax.el without fixing up any of the references. Commit 30b58d43e48569afb50a35d3915ec7d453a61f5d only fixed up some of them. Here are some more (hopefully all of them). Signed-off-by: Anders Kaseorg <andersk@mit.edu>
* Coq_makefile: Allow empty logical namesGravatar Pierre Boutillier2014-10-09
| | | | I'm not sure that coqdep and coqtop understand them correctly anyway ...
* Applying Virgile Prevosto's patch for better error report in coqdep (#3029).Gravatar Hugo Herbelin2014-10-08
|
* coq_makefile: explicit target install-toploop for toploop pluginsGravatar Enrico Tassi2014-10-07
|
* fix wrong escaping in coq_makefileGravatar Enrico Tassi2014-10-06
|
* coq_makefile: build and install *top.cmxs pluginsGravatar Enrico Tassi2014-10-01
| | | | | | | | These plugins, like coqidetop, stmworkertop and tacworkertop are intended for toploop replacements (see -toploop command line option). With this commit coq_makefile can be used as the build system for any user-interface-specific plugins.
* fix coq_makefileGravatar Pierre Boutillier2014-09-18
|
* Revert "coqc: execvp is now available even on win32"Gravatar Enrico Tassi2014-09-17
| | | | | | | | | This reverts commit 60c390951cb2d771c16758a84bf592d06769da14. The reason is that execvp exists on windows but is "non blocking". So coqc would detach "coqtop -compile" and make would fail trying to step to the next target before "coqtop -compile" terminates (because coqc did terminate already).
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
| | | | Involves changing the [mind_finite] field in the kernel from a bool to the trivalued type [Decl_kinds.recursivity_kind]. This is why so many files are (unfortunately) affected. It would not be very surprising if some bug was introduced.
* Add a [Variant] declaration which allows to write non-recursive variant types.Gravatar Arnaud Spiwack2014-09-04
| | | | Just like the [Record] keyword allows only non-recursive records.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 15:35:58 +0000