Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-10-02 |
|\ | |||
* \ | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-10-02 |
|\ \ | |||
| | * | Universes: enforce Set <= i for all Type occurrences. | Matthieu Sozeau | 2015-10-02 |
| |/ | |||
| * | Build the compatibility files. | Guillaume Melquiond | 2015-09-30 |
| | | |||
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-09-25 |
|\| | |||
| * | Updating the documentation and the toolchain w.r.t. the change in -compile. | Pierre-Marie Pédrot | 2015-09-25 |
| | | |||
| * | Revert changes in Makefile.build done as part of 2bc88f9a. | Maxime Dénès | 2015-09-17 |
| | | | | | | | | If it was intentional, please commit again separately. | ||
| * | Univs: Add universe binding lists to definitions | Matthieu Sozeau | 2015-09-14 |
| | | | | | | | | | | ... lemmas and inductives to control which universes are bound and where in universe polymorphic definitions. Names stay outside the kernel. | ||
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-09-06 |
|\| | |||
| * | Adding a Makefile target for the MSets and MMaps directories. | Pierre-Marie Pédrot | 2015-09-06 |
| | | | | | | | | | | The target creation process should eventually be automated, because it is tedious and error-prone as witnessed by this commit. | ||
* | | Fixing generation of dev/printers.mllib.d after ocamllibdep is used ↵ | Hugo Herbelin | 2015-08-29 |
| | | | | | | | | (48d611ff2a). | ||
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-07-27 |
|\| | |||
| * | Silence `which` | Jason Gross | 2015-07-23 |
| | | | | | | | | On Fedora, `which 2>&1 >/dev/null` doesn't silence stderr, while `which >/dev/null 2>&1` does. | ||
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-07-18 |
|\| | |||
| * | Updating checksum in checker (9c732a5cc continued). | Hugo Herbelin | 2015-07-12 |
| | | | | | | | | | | | | Calling md5sum test earlier, at the time coqchk is built, rather than at testing time, hopefully moving it closer to what it is supposed to occur. | ||
* | | Merge branch 'v8.5' into trunk | Maxime Dénès | 2015-07-02 |
|\| | |||
| * | Revert "Add target to install dev files." | Maxime Dénès | 2015-07-02 |
| | | | | | | | | | | | | Broke the build. This reverts commit ef6459b00999a29183edc09de9035795ff7912e9. | ||
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-06-28 |
|\| | |||
| * | Add target to install dev files. | Matthieu Sozeau | 2015-06-26 |
| | | |||
| * | Adding a more efficient representation of OCaml objects in votour. | Pierre-Marie Pédrot | 2015-06-25 |
| | | |||
| * | More silent Makefile when looking for codesign. | Maxime Dénès | 2015-06-24 |
| | | | | | | | | May still be wrong on Windows, though. | ||
* | | All invocations to ocaml compilers go through ocamlfind | Pierre Boutillier | 2015-06-22 |
| | | | | | | | | | | Nothing is done for camlp4 There is an issue with computing camlbindir | ||
* | | Merge v8.5 into trunk | Hugo Herbelin | 2015-05-15 |
|\| | | | | | | | | | | | | | Conflicts: tactics/eauto.ml4 (merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API) | ||
| * | Disable precompilation for native_compute by default. | Guillaume Melquiond | 2015-05-14 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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. | ||
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-04-15 |
|\| | |||
| * | Fix compilation broken by Matthieu's last commit. | Pierre Letouzey | 2015-04-10 |
| | | | | | | | | | | | | | | | | Btw, also unset the READABLE_ML4 option, which probably caused this issue. No, we normally do *not* want to see the internals of .ml generated out of a .ml4 (except during some specific debug sessions). It is *so* easy otherwise to edit the wrong .ml by mistake and forget to edit the original .ml4. | ||
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-03-23 |
|\| | |||
| * | Fix Bug 3548 - Makefile should fallback gracefully in the absence of codesign | Pierre Boutillier | 2015-03-14 |
| | | |||
* | | Adding a new folder corresponding to the low-level part of the pretyper | Pierre-Marie Pédrot | 2015-02-27 |
| | | | | | | | | | | | | | | together with the tactic monad. The move is not complete yet, because some file candidates for this directory have almost useless dependencies in other ones that should not be moved. | ||
* | | Using home-made ocamllibdep rather than coqdep_boot. | Hugo Herbelin | 2015-02-16 |
| | | |||
* | | Restricting the need for coqdep_boot to mllib.d files (since ocaml | Hugo Herbelin | 2015-02-16 |
|/ | | | | | 3.12.1, ocamldep was able to deal with .ml4, so that building .mllib.d is the only feature that coqdep_boot was still required for). | ||
* | Fixup version & copyright for MacOS bundle | Pierre Boutillier | 2015-02-13 |
| | |||
* | Revert "Using same code for browsing physical directories in coqtop and coqdep." | Hugo Herbelin | 2015-02-12 |
| | | | | | | (Sorry, was not intended to be pushed) This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c. | ||
* | Using same code for browsing physical directories in coqtop and coqdep. | Hugo Herbelin | 2015-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). | ||
* | Always build (even when -coqide no) and install idetoploop | Pierre Boutillier | 2015-01-15 |
| | | | | So you can link a coqtop compiled (by opam) without coqide to a stand alone coqide (binary distributed) | ||
* | Makefile: install ide/*lang | Enrico Tassi | 2015-01-14 |
| | |||
* | typo in coqide compilation rules after -thread requirement | Pierre Boutillier | 2015-01-12 |
| | |||
* | Fixing Makefile so that it puts the -thread flag on the right place. | Pierre-Marie Pédrot | 2014-12-17 |
| | |||
* | Revert and correctly fix "#4843 part 2 : The .cmxs files for plugins must ↵ | Pierre Boutillier | 2014-12-17 |
| | | | | | | have x permission" This reverts commit 607503b28fca50f4b76b2237d5ca13802b8252fa. | ||
* | Proper thread-safe implementation for Exninfo. | Pierre-Marie Pédrot | 2014-12-16 |
| | | | | | This is the second part of the Exninfo patch. It introduces dependency in the Thread library in all Coq files. | ||
* | #4843 part 2 : The .cmxs files for plug-ins must have execute permission | Pierre Boutillier | 2014-12-12 |
| | |||
* | win32: bring back the coq icon in the coqide binary | Enrico Tassi | 2014-09-17 |
| | |||
* | IDECDEPSFLAGS is for byte, not opt | Enrico Tassi | 2014-09-09 |
| | |||
* | Removing the XML plugin. | Pierre-Marie Pédrot | 2014-09-08 |
| | | | | | Left a README, just in case someone will discover the remnants of it decades from now. | ||
* | Make CoqIDE compile with windows (Closes: 3573) | Enrico Tassi | 2014-09-04 |
| | | | | | | CoqIDE seems to work, but for random pauses that make you think of a thread deadlock, but then, after a few seconds, things make progress again. This happens only seldom on my virtual machine. | ||
* | coqworkmgr | Enrico Tassi | 2014-09-02 |
| | |||
* | Distributed binaries under MacOS are signed. | Pierre Boutillier | 2014-08-26 |
| | |||
* | Fixing ml-dot & mli-dot targets. | Pierre-Marie Pédrot | 2014-08-23 |
| | |||
* | fixup fakeide test-suite | Pierre Boutillier | 2014-07-24 |
| | |||
* | A makefile rule to build bin/CoqIDE_$VERSION.app macOS bundle | Pierre Boutillier | 2014-07-22 |
| | | | | The created bundle contains only coqide and gtk (no coqtop, no stdlib) |