aboutsummaryrefslogtreecommitdiff
path: root/Makefile.build
AgeCommit message (Expand)Author
2021-04-19[build] Remove leftovers of codesigning / OSX IDe infrastructure.Emilio Jesus Gallego Arias
2021-04-12Fix unknown -vos option for coqdep_boot introduced in PR #11074Hendrik Tews
2021-02-19Add a file coq_arity.h generated by genOpcodeFiles.ml.Guillaume Melquiond
2020-11-20Build all_stdlib.v in test suite makefileGaëtan Gilbert
2020-10-06Use OCaml floating-point operations on 64 bits archPierre Roux
2020-09-17[build] Don't link `num` anymore in CoqEmilio Jesus Gallego Arias
2020-08-27[nsatz] num → zarithVincent Laporte
2020-08-27[numeral] [plugins] Switch from `Big_int` to ZArith.Emilio Jesus Gallego Arias
2020-08-18Rename VM-related kernel/cfoo files to kernel/vmfooGaëtan Gilbert
2020-06-02Move CoqIDE to its own folderMaxime Dénès
2020-05-06Fix #12211Jason Gross
2020-04-29When TIMED=1, emit timing info for OCaml filesJason Gross
2020-04-24Add memory stats to tables by defaultJason Gross
2020-04-21Merge PR #12082: Fixes #11808: support for test-suite in -byte-only modeGaëtan Gilbert
2020-04-20TIMEFMT: Display the output file nameJason Gross
2020-04-19Fix Makefile warning: undefined variable '*'Jason Gross
2020-04-12Fixing export of CAML_LD_LIBRARY_PATH from config/Makefile to Makefile.common.Hugo Herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-04[micromega] Add numerical compatibility layer.Emilio Jesus Gallego Arias
2020-03-02Merge PR #11634: Remove the dependency in float.cmo and uint63.cmo for buildi...Pierre-Marie Pédrot
2020-02-19Merge PR #11302: Add --fuzz, --real, --user to timing scriptsEmilio Jesus Gallego Arias
2020-02-19Remove the dependency in float.cmo and uint63.cmo for building votour.Hugo Herbelin
2020-02-13[build] Consolidate stdlib's .v files under a single directory.Emilio Jesus Gallego Arias
2020-02-07[coqdep] Don't treat stdlib specially in boot mode.Emilio Jesus Gallego Arias
2020-02-05Add --fuzz, --real, --user to timing scriptsJason Gross
2020-01-30Don't install doc_grammarGaëtan Gilbert
2019-12-12Fix #11195 and add other improvements: try loading .vio (and not just .vo) if...charguer
2019-11-21Merge PR #10614: Update the Gallina grammar in doc, "Terms" sectionThéo Zimmermann
2019-11-20Update grammar in the Terms section of Gallina chapterJim Fehrle
2019-11-08coqdep: only output vos when passed -vosGaëtan Gilbert
2019-11-01Makefile.build: Fix rules of bin/votour{,.byte}Erik Martin-Dorel
2019-11-01Make primitive float work on x86_32Pierre Roux
2019-11-01Add primitive floats to checkerPierre Roux
2019-10-18Adding a test for votour.Pierre-Marie Pédrot
2019-10-14Merge PR #10811: Allow SProp default onPierre-Marie Pédrot
2019-10-12[make] separate generated gramlib ml files from mli files (fix #10864)Enrico Tassi
2019-10-04Allow SProp default onGaëtan Gilbert
2019-10-03Improved handling of micromega cachesFrédéric Besson
2019-08-25Changed chmod -w to chmod a-w to avoid error on cygwinMichael Soegtrop
2019-08-24saner cond_flags in makefileGaëtan Gilbert
2019-08-24Simplify picking between uint63_63.ml and uint63_31.mlGaëtan Gilbert
2019-07-19Introduce doc_gram, a utilty for extracting Coq's grammar from .mlg filesJim Fehrle
2019-06-17Update py-style headers to new year.Théo Zimmermann
2019-06-06Merge PR #9972: [build] Select uint63 using `ocamlc -config` variables.Vincent Laporte
2019-05-21Fixing typos - Part 1JPR
2019-05-21[build] Select uint63 using `ocamlc -config` variables.Emilio Jesus Gallego Arias
2019-05-07Integrate build and documentation of Ltac2Maxime Dénès
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-03-11Fix undefined gramlib_MLLIB_DEPENDENCIES in make installGaëtan Gilbert
2019-03-03Cleanup exported variables in Makefile.buildGaëtan Gilbert