index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Makefile.build
Age
Commit message (
Expand
)
Author
2021-04-19
[build] Remove leftovers of codesigning / OSX IDe infrastructure.
Emilio Jesus Gallego Arias
2021-04-12
Fix unknown -vos option for coqdep_boot introduced in PR #11074
Hendrik Tews
2021-02-19
Add a file coq_arity.h generated by genOpcodeFiles.ml.
Guillaume Melquiond
2020-11-20
Build all_stdlib.v in test suite makefile
Gaëtan Gilbert
2020-10-06
Use OCaml floating-point operations on 64 bits arch
Pierre Roux
2020-09-17
[build] Don't link `num` anymore in Coq
Emilio Jesus Gallego Arias
2020-08-27
[nsatz] num → zarith
Vincent Laporte
2020-08-27
[numeral] [plugins] Switch from `Big_int` to ZArith.
Emilio Jesus Gallego Arias
2020-08-18
Rename VM-related kernel/cfoo files to kernel/vmfoo
Gaëtan Gilbert
2020-06-02
Move CoqIDE to its own folder
Maxime Dénès
2020-05-06
Fix #12211
Jason Gross
2020-04-29
When TIMED=1, emit timing info for OCaml files
Jason Gross
2020-04-24
Add memory stats to tables by default
Jason Gross
2020-04-21
Merge PR #12082: Fixes #11808: support for test-suite in -byte-only mode
Gaëtan Gilbert
2020-04-20
TIMEFMT: Display the output file name
Jason Gross
2020-04-19
Fix Makefile warning: undefined variable '*'
Jason Gross
2020-04-12
Fixing export of CAML_LD_LIBRARY_PATH from config/Makefile to Makefile.common.
Hugo Herbelin
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2020-03-04
[micromega] Add numerical compatibility layer.
Emilio Jesus Gallego Arias
2020-03-02
Merge PR #11634: Remove the dependency in float.cmo and uint63.cmo for buildi...
Pierre-Marie Pédrot
2020-02-19
Merge PR #11302: Add --fuzz, --real, --user to timing scripts
Emilio Jesus Gallego Arias
2020-02-19
Remove 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-05
Add --fuzz, --real, --user to timing scripts
Jason Gross
2020-01-30
Don't install doc_grammar
Gaëtan Gilbert
2019-12-12
Fix #11195 and add other improvements: try loading .vio (and not just .vo) if...
charguer
2019-11-21
Merge PR #10614: Update the Gallina grammar in doc, "Terms" section
Théo Zimmermann
2019-11-20
Update grammar in the Terms section of Gallina chapter
Jim Fehrle
2019-11-08
coqdep: only output vos when passed -vos
Gaëtan Gilbert
2019-11-01
Makefile.build: Fix rules of bin/votour{,.byte}
Erik Martin-Dorel
2019-11-01
Make primitive float work on x86_32
Pierre Roux
2019-11-01
Add primitive floats to checker
Pierre Roux
2019-10-18
Adding a test for votour.
Pierre-Marie Pédrot
2019-10-14
Merge PR #10811: Allow SProp default on
Pierre-Marie Pédrot
2019-10-12
[make] separate generated gramlib ml files from mli files (fix #10864)
Enrico Tassi
2019-10-04
Allow SProp default on
Gaëtan Gilbert
2019-10-03
Improved handling of micromega caches
Frédéric Besson
2019-08-25
Changed chmod -w to chmod a-w to avoid error on cygwin
Michael Soegtrop
2019-08-24
saner cond_flags in makefile
Gaëtan Gilbert
2019-08-24
Simplify picking between uint63_63.ml and uint63_31.ml
Gaëtan Gilbert
2019-07-19
Introduce doc_gram, a utilty for extracting Coq's grammar from .mlg files
Jim Fehrle
2019-06-17
Update py-style headers to new year.
Théo Zimmermann
2019-06-06
Merge PR #9972: [build] Select uint63 using `ocamlc -config` variables.
Vincent Laporte
2019-05-21
Fixing typos - Part 1
JPR
2019-05-21
[build] Select uint63 using `ocamlc -config` variables.
Emilio Jesus Gallego Arias
2019-05-07
Integrate build and documentation of Ltac2
Maxime Dénès
2019-03-14
Add a non-cumulative impredicative universe SProp.
Gaëtan Gilbert
2019-03-11
Fix undefined gramlib_MLLIB_DEPENDENCIES in make install
Gaëtan Gilbert
2019-03-03
Cleanup exported variables in Makefile.build
Gaëtan Gilbert
[next]