aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.build
Commit message (Collapse)AuthorAge
...
* | Ensuring that documentation of mli code works in the presence of utf-8Gravatar Hugo Herbelin2015-12-05
| | | | | | | | characters.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-03
|\|
| * Adding a target report to test-suite's Makefile to get a short summary.Gravatar Hugo Herbelin2015-12-02
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\|
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\ \
| | * Universes: enforce Set <= i for all Type occurrences.Gravatar Matthieu Sozeau2015-10-02
| |/
| * Build the compatibility files.Gravatar Guillaume Melquiond2015-09-30
| |
* | 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
| |
| * Revert changes in Makefile.build done as part of 2bc88f9a.Gravatar Maxime Dénès2015-09-17
| | | | | | | | If it was intentional, please commit again separately.
| * Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-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'Gravatar Pierre-Marie Pédrot2015-09-06
|\|
| * Adding a Makefile target for the MSets and MMaps directories.Gravatar Pierre-Marie Pédrot2015-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 ↵Gravatar Hugo Herbelin2015-08-29
| | | | | | | | (48d611ff2a).
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-07-27
|\|
| * Silence `which`Gravatar Jason Gross2015-07-23
| | | | | | | | On Fedora, `which 2>&1 >/dev/null` doesn't silence stderr, while `which >/dev/null 2>&1` does.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-07-18
|\|
| * Updating checksum in checker (9c732a5cc continued).Gravatar Hugo Herbelin2015-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 trunkGravatar Maxime Dénès2015-07-02
|\|
| * Revert "Add target to install dev files."Gravatar Maxime Dénès2015-07-02
| | | | | | | | | | | | Broke the build. This reverts commit ef6459b00999a29183edc09de9035795ff7912e9.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-06-28
|\|
| * Add target to install dev files.Gravatar Matthieu Sozeau2015-06-26
| |
| * Adding a more efficient representation of OCaml objects in votour.Gravatar Pierre-Marie Pédrot2015-06-25
| |
| * More silent Makefile when looking for codesign.Gravatar Maxime Dénès2015-06-24
| | | | | | | | May still be wrong on Windows, though.
* | All invocations to ocaml compilers go through ocamlfindGravatar Pierre Boutillier2015-06-22
| | | | | | | | | | Nothing is done for camlp4 There is an issue with computing camlbindir
* | Merge v8.5 into trunkGravatar Hugo Herbelin2015-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.Gravatar Guillaume Melquiond2015-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'Gravatar Pierre-Marie Pédrot2015-04-15
|\|
| * Fix compilation broken by Matthieu's last commit.Gravatar Pierre Letouzey2015-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'Gravatar Pierre-Marie Pédrot2015-03-23
|\|
| * Fix Bug 3548 - Makefile should fallback gracefully in the absence of codesignGravatar Pierre Boutillier2015-03-14
| |
* | Adding a new folder corresponding to the low-level part of the pretyperGravatar Pierre-Marie Pédrot2015-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.Gravatar Hugo Herbelin2015-02-16
| |
* | Restricting the need for coqdep_boot to mllib.d files (since ocamlGravatar Hugo Herbelin2015-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 bundleGravatar Pierre Boutillier2015-02-13
|
* 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.
* 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).
* Always build (even when -coqide no) and install idetoploopGravatar Pierre Boutillier2015-01-15
| | | | So you can link a coqtop compiled (by opam) without coqide to a stand alone coqide (binary distributed)
* Makefile: install ide/*langGravatar Enrico Tassi2015-01-14
|
* typo in coqide compilation rules after -thread requirementGravatar Pierre Boutillier2015-01-12
|
* Fixing Makefile so that it puts the -thread flag on the right place.Gravatar Pierre-Marie Pédrot2014-12-17
|
* Revert and correctly fix "#4843 part 2 : The .cmxs files for plugins must ↵Gravatar Pierre Boutillier2014-12-17
| | | | | | have x permission" This reverts commit 607503b28fca50f4b76b2237d5ca13802b8252fa.
* Proper thread-safe implementation for Exninfo.Gravatar Pierre-Marie Pédrot2014-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 permissionGravatar Pierre Boutillier2014-12-12
|
* win32: bring back the coq icon in the coqide binaryGravatar Enrico Tassi2014-09-17
|
* IDECDEPSFLAGS is for byte, not optGravatar Enrico Tassi2014-09-09
|
* Removing the XML plugin.Gravatar Pierre-Marie Pédrot2014-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)Gravatar Enrico Tassi2014-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.
* coqworkmgrGravatar Enrico Tassi2014-09-02
|
* Distributed binaries under MacOS are signed.Gravatar Pierre Boutillier2014-08-26
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 12:14:14 +0000