aboutsummaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Expand)Author
2016-08-19Unify location handling of error functions.Emilio Jesus Gallego Arias
2016-08-09Make List.map_filter(_i) tail-recursive.Guillaume Melquiond
2016-07-08Fixing the printing of unknown locations by adding a newline.Pierre-Marie Pédrot
2016-07-08Adding a breaking space in warning names.Pierre-Marie Pédrot
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-06-27Merge remote-tracking branch 'github/pr/223' into feedback-locationsMaxime Dénès
2016-06-27add CList.extract_firstGabriel Scherer
2016-06-25[feedback] Remove `ErrorMsg` in favor of `Message Error`.Emilio Jesus Gallego Arias
2016-06-25[feedback] Allow messages to carry a location.Emilio Jesus Gallego Arias
2016-06-25[feedback] Add optional ?loc parameter to loggers.Emilio Jesus Gallego Arias
2016-06-25[feedback] Remove unused tag on `Debug` level.Emilio Jesus Gallego Arias
2016-06-20Add file name, line number and beginning of line position to locations.Maxime Dénès
2016-06-17remote counter: avoid thread race on sockets (fix #4823)Enrico Tassi
2016-06-17remote counter: avoid thread race on sockets (fix #4823)Enrico Tassi
2016-06-16Merge 'pr/191' into trunkEnrico Tassi
2016-06-14Preventive compatibility fixes for flushing.Emilio Jesus Gallego Arias
2016-06-14Merge remote-tracking branch 'origin/pr/166' into trunkEnrico Tassi
2016-06-14-async-proofs-delegation-threshold default value set to 0.03Enrico Tassi
2016-06-14Merge remote-tracking branch 'origin/pr/182' into trunkEnrico Tassi
2016-06-14Merge remote-tracking branch 'origin/pr/173' into trunkEnrico Tassi
2016-06-14Add a [CList.partitioni] function.Cyprien Mangin
2016-06-14Merge branch "LtacProf for trunk" (PR #165).Pierre-Marie Pédrot
2016-06-14Moving back Ltac profiling to the Ltac folder.Pierre-Marie Pédrot
2016-06-14Moving UTF-8 related functions to Unicode module.Pierre-Marie Pédrot
2016-06-13Revert "Strip some trailing spaces"Pierre-Marie Pédrot
2016-06-09Adding a bit of documentation in the mli.Pierre-Marie Pédrot
2016-06-07DocumentationEnrico Tassi
2016-06-06STM: each proof block can be enabled separatelyEnrico Tassi
2016-06-06STM: proof block detection made optional + simple testEnrico Tassi
2016-06-06STM: support for nested boxes of nodes to model error boundariesEnrico Tassi
2016-06-05LtacProf for Coq trunkJason Gross
2016-06-05Strip some trailing spacesJason Gross
2016-06-04Merge remote-tracking branch 'github/pr/184' into trunkMaxime Dénès
2016-06-02Please never mention .mli-only file in *.mllib (or future *.mlpack)Pierre Letouzey
2016-06-02Add documentation to the low-level `Pp` functions.Emilio Jesus Gallego Arias
2016-06-02Move ide serialization libraries from lib/ to ide/Emilio Jesus Gallego Arias
2016-06-02Encapsulate xml serialization in xmlprotocol.mliEmilio Jesus Gallego Arias
2016-06-02Remove tabulation support from pretty-printing.Guillaume Melquiond
2016-06-01Merge branch 'yet-another-makefile-bigbang' into trunkPierre Letouzey
2016-06-01Makefile: restore the use of coqdep_boot for creating .v.d filesPierre Letouzey
2016-05-31STM delegation policy can be customizedEnrico Tassi
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-19Unicode.ascii_of_ident is now truly injectivePierre Letouzey
2016-05-19Unicode.ascii_of_ident is now truly injectivePierre Letouzey
2016-05-19coqc: support -o option to specify output file nameEnrico Tassi
2016-05-13Dyn: simplify API introducing an Easy submoduleEnrico Tassi
2016-05-12Fix bug #4722: Coq dies when encountering broken symbolic links.Pierre-Marie Pédrot
2016-05-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot