aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
Commit message (Collapse)AuthorAge
...
* 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.
* coqworkmgrGravatar Enrico Tassi2014-09-02
|
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
| | | | | | | | | | | It's possible that I should have removed more "allows", as many instances of "foo allows to bar" could have been replaced by "foo bars" (e.g., "[Qed] allows to check and save a complete proof term" could be "[Qed] checks and saves a complete proof term"), but not always (e.g., "the optional argument allows to ignore universe polymorphism" should not be "the optional argument ignores universe polymorphism" but "the optional argument allows the caller to instruct Coq to ignore universe polymorphism" or something similar).
* factored out require_modifiers + bug fix.Gravatar Gregory Malecha2014-08-25
| | | | | Conflicts: tools/coqdep_lexer.mll
* coqdep comments counter is in the stackGravatar Pierre Boutillier2014-08-25
|
* a comment about the new state.Gravatar Gregory Malecha2014-08-25
|
* Support for Timeout n and From ..Gravatar Gregory Malecha2014-08-25
| | | | | - The state machine gets kind of complex maybe it should become a parser at some point?
* Make coqdep find Require commands prefixed by TimeGravatar Gregory Malecha2014-08-25
|
* Make beautify-archive usable on non-GNU systems.Gravatar Xavier Clerc2014-08-21
|
* fixup fakeide test-suiteGravatar Pierre Boutillier2014-07-24
|
* Coq_makefile: fix cmx compilation when there are both ml and mllibGravatar Pierre Boutillier2014-07-07
|
* Fix Coq_makefile in presence of mlpackGravatar Pierre Boutillier2014-07-03
|
* coqdoc is minimaly -Q awareGravatar Pierre Boutillier2014-07-03
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 08:23:02 +0000