| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-01-27 | Fixed a wrong warning in coq_makefile. | Pierre Courtieu | |
| A non empty dir detected as an empty one. | |||
| 2015-01-27 | Allow -type-in-type to be an option also for coqc. | Daniel R. Grayson | |
| 2015-01-16 | coq_makefile: install also .v and .glob | Enrico Tassi | |
| 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 | |||
| 2015-01-15 | Remove left-over dead code in previous commit. | Maxime Dénès | |
| 2015-01-15 | Make -print-mod-uid accept a list of files. | Maxime Dénès | |
| Solves an efficiency problem in Makefiles generated by coq_makefile. | |||
| 2015-01-15 | Make installation of native files more robust. | Maxime Dénès | |
| 2015-01-15 | coq_makefile installs native files | Pierre Boutillier | |
| 2015-01-14 | coq_makefile: chmod 755 on toplopp cmxs | Enrico Tassi | |
| 2015-01-13 | Made -print-mod-uid more silent and robust. | Maxime Dénès | |
| This is a follow-up on Pierre's 5d80a385. | |||
| 2015-01-12 | Coq_makefile erases native compiler files | Pierre Boutillier | |
| 2015-01-12 | Update headers. | Maxime Dénès | |
| 2015-01-12 | Fixing typo in previous commit. | Hugo Herbelin | |
| 2015-01-11 | Fixing wrong duplication message when finding both a .ml and a .ml4 in coqdep. | Hugo Herbelin | |
| 2015-01-06 | rename: vi -> vio | Enrico Tassi | |
| 2015-01-06 | Improve error recovery in case of ill-formed coqdoc comment. (Fix for bug ↵ | Guillaume Melquiond | |
| #3802.) | |||
| 2014-12-25 | Inlining Spawn.kill_if in the one place were it was actually used, thus | Pierre-Marie Pédrot | |
| removing the need of thread creation in the interface. | |||
| 2014-12-18 | Bug fix (coq_makefile): Adding unix.cma and threads.cma dependencies for ↵ | mlasson | |
| grammar in campl4 | |||
| 2014-12-15 | Fixing bug #3865. | Pierre-Marie Pédrot | |
| 2014-12-12 | Fix #3800 : cmxs need execution priviledges under windows | Pierre Boutillier | |
| 2014-12-09 | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey | |
| 2014-12-09 | coqdoc.css: fix a few errors | Pierre Letouzey | |
| 2014-12-09 | coqdoc: fix a few issues with xhtml validity (backport 1636f7 and 754abf1 ↵ | Pierre Letouzey | |
| 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 /> | |||
| 2014-12-09 | Port to trunk commit r16062 of v8.4 (Correction des entêtes pour la ↵ | notin | |
| documentation en ligne) | |||
| 2014-12-04 | coqdep: granting #2506 (./dir is the same as dir) | Hugo Herbelin | |
| 2014-12-04 | coqdep: Warning about ml file clashes, keeping the file corresponding | Hugo Herbelin | |
| 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. | |||
| 2014-10-27 | Use the url package, since coqdoc generates \url commands. | Guillaume Melquiond | |
| 2014-10-22 | Supporting Greek and Coptic (U0370) as first letter of coqdoc identifiers. | Hugo Herbelin | |
| 2014-10-16 | More fallout from elisp rename | Anders Kaseorg | |
| 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> | |||
| 2014-10-09 | Coq_makefile: Allow empty logical names | Pierre Boutillier | |
| I'm not sure that coqdep and coqtop understand them correctly anyway ... | |||
| 2014-10-08 | Applying Virgile Prevosto's patch for better error report in coqdep (#3029). | Hugo Herbelin | |
| 2014-10-07 | coq_makefile: explicit target install-toploop for toploop plugins | Enrico Tassi | |
| 2014-10-06 | fix wrong escaping in coq_makefile | Enrico Tassi | |
| 2014-10-01 | coq_makefile: build and install *top.cmxs plugins | Enrico Tassi | |
| 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. | |||
| 2014-09-18 | fix coq_makefile | Pierre Boutillier | |
| 2014-09-17 | Revert "coqc: execvp is now available even on win32" | Enrico Tassi | |
| 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). | |||
| 2014-09-04 | Print [Variant] types with the keyword [Variant]. | Arnaud Spiwack | |
| 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. | |||
| 2014-09-04 | Add a [Variant] declaration which allows to write non-recursive variant types. | Arnaud Spiwack | |
| Just like the [Record] keyword allows only non-recursive records. | |||
| 2014-09-02 | coqworkmgr | Enrico Tassi | |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross | |
| 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). | |||
| 2014-08-25 | factored out require_modifiers + bug fix. | Gregory Malecha | |
| Conflicts: tools/coqdep_lexer.mll | |||
| 2014-08-25 | coqdep comments counter is in the stack | Pierre Boutillier | |
| 2014-08-25 | a comment about the new state. | Gregory Malecha | |
| 2014-08-25 | Support for Timeout n and From .. | Gregory Malecha | |
| - The state machine gets kind of complex maybe it should become a parser at some point? | |||
| 2014-08-25 | Make coqdep find Require commands prefixed by Time | Gregory Malecha | |
| 2014-08-21 | Make beautify-archive usable on non-GNU systems. | Xavier Clerc | |
| 2014-07-24 | fixup fakeide test-suite | Pierre Boutillier | |
| 2014-07-07 | Coq_makefile: fix cmx compilation when there are both ml and mllib | Pierre Boutillier | |
| 2014-07-03 | Fix Coq_makefile in presence of mlpack | Pierre Boutillier | |
| 2014-07-03 | coqdoc is minimaly -Q aware | Pierre Boutillier | |
| 2014-07-03 | Bug 3405: Coq_makefile: Implicit rules only for listed files in Make file | Pierre Boutillier | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |