aboutsummaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Expand)Author
2019-02-11Merge PR #9478: Remove the comment fields of locations.Emilio Jesus Gallego Arias
2019-02-08Merge PR #9525: Remove global output_native_objects flag.Emilio Jesus Gallego Arias
2019-02-08Merge PR #9523: Make boot flag into a normal option (no global flag).Emilio Jesus Gallego Arias
2019-02-08Remove global output_native_objects flag.Gaëtan Gilbert
2019-02-08Make boot flag into a normal option (no global flag).Gaëtan Gilbert
2019-02-05Remove the comment fields of locations.Pierre-Marie Pédrot
2019-02-05Make Program a regular attributeMaxime Dénès
2019-01-27Merge PR #9263: [STM] explicit handling of parsing statesEmilio Jesus Gallego Arias
2019-01-24Update -compat to support -compat 8.10Jason Gross
2019-01-24[STM] API to print a Stateid.tEnrico Tassi
2019-01-24Merge PR #9372: [thread] protect threads against sigalrmEmilio Jesus Gallego Arias
2019-01-22[thread] protect threads against sigalrmEnrico Tassi
2019-01-22Make prvect tail recursive (fix #9355)Gaëtan Gilbert
2019-01-08Fix #3934: coqc -time -quick gives unreadable outputMaxime Dénès
2018-12-25Adding a comparison combinator for pairs.Hugo Herbelin
2018-12-18Add comment to acyclicgraph APIGaëtan Gilbert
2018-12-17Remove universe specific terminology from acyclicgraphGaëtan Gilbert
2018-12-17Make ugraph implementation abstract wrt universe specificsGaëtan Gilbert
2018-12-12Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comme...Maxime Dénès
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-12-08Do so that an error message follows the "Error:" header on the same line.Hugo Herbelin
2018-12-05Merge PR #9065: [gramlib] Remove `Ploc.t` in favor of `Loc.t`Pierre-Marie Pédrot
2018-12-04Remove leftover code that used to handle ml4 files.Pierre-Marie Pédrot
2018-11-30[gramlib] Remove `Ploc.t` in favor of `Loc.t`Emilio Jesus Gallego Arias
2018-11-30Merge PR #9068: [dune] Minor tweak of dependencies.Théo Zimmermann
2018-11-27[lib] Remove leftover flag `print_mod_uid`Emilio Jesus Gallego Arias
2018-11-26[dune] Minor tweak of dependencies.Emilio Jesus Gallego Arias
2018-11-22Merge PR #8967: Fix #8922 (uncaught pp_diff exception)Hugo Herbelin
2018-11-21[camlp5] Remove dependency on camlp5.Emilio Jesus Gallego Arias
2018-11-18[options] Remove deprecated option automatic introduction.Emilio Jesus Gallego Arias
2018-11-17[CoqProject] Abstract warning function for CoqProject readers.Emilio Jesus Gallego Arias
2018-11-14Get hyps and goal the same way Printer does; don't omit infoJim Fehrle
2018-11-12[clib] Remove unneeded `get_extension` function.Emilio Jesus Gallego Arias
2018-11-08Ensure termination of `file_exists_respecting_case`Vincent Laporte
2018-11-02Universe Polymorphism is a normal attribute modulo the stm (no Flags)Gaëtan Gilbert
2018-10-29Merge PR #8763: Adapt coq_makefile to handle coqpp-based macro files.Enrico Tassi
2018-10-23[build] Refactoring to config lib and ocamldebug tweaks.Emilio Jesus Gallego Arias
2018-10-19Adapt coq_makefile to handle coqpp-based macro files.Pierre-Marie Pédrot
2018-10-16[clib] Deprecate string functions available in OCaml 4.05Emilio Jesus Gallego Arias
2018-10-15Correct some spelling errorsBenjamin Barenblat
2018-10-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-10-02Update the -compat flagsJason Gross
2018-10-01[envars] Small implementation cleanup for coqlib internals.Emilio Jesus Gallego Arias
2018-10-01[lib] [flags] Move coqlib handling out of `Flags`Emilio Jesus Gallego Arias
2018-10-01[lib] [flags] Move private IDE functions to `ide`Emilio Jesus Gallego Arias
2018-10-01[envars] Defer CAMLP5 location to configure.Emilio Jesus Gallego Arias
2018-09-27[coqc] Use standard binary location routine from libEmilio Jesus Gallego Arias
2018-09-10[dune] Add apidoc target using `odoc`Emilio Jesus Gallego Arias
2018-09-05[bin] Fix binary location procedure to work with symlinks.Emilio Jesus Gallego Arias
2018-09-05[build] Preliminary support for building Coq with `dune`.Emilio Jesus Gallego Arias