aboutsummaryrefslogtreecommitdiff
path: root/checker/check.mllib
AgeCommit message (Expand)Author
2020-04-16Checker: factorize handling of typing flagsGaëtan Gilbert
2018-11-06[checker] Refactor by sharing code with the kernelMaxime Dénès
2018-10-23[build] Refactoring to config lib and ocamldebug tweaks.Emilio Jesus Gallego Arias
2018-06-18Remove Canary.whitequark
2017-11-28Use safe demarshalling in the checker.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-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-31Feedback cleanupEmilio Jesus Gallego Arias
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-04Rename Ephemeron -> CEphemeron.Maxime Dénès
2016-01-06Merge remote-tracking branch 'origin/v8.5' into trunkGuillaume Melquiond
2016-01-05Fix order of files in mllib.Maxime Dénès
2015-12-05Factorizing unsafe code by relying on the new Dyn module.Pierre-Marie Pédrot
2015-06-25Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Thomas Sibut-Pinote
2015-06-23Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Thomas Sibut-Pinote
2015-02-16Using same code for browsing physical directories in coqtop and coqdep.Hugo Herbelin
2015-02-12Revert "Using same code for browsing physical directories in coqtop and coqdep."Hugo Herbelin
2015-02-12Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)Hugo Herbelin
2015-02-12Capital letter in plugins.Hugo Herbelin
2015-02-12Using same code for browsing physical directories in coqtop and coqdep.Hugo Herbelin
2014-08-04STM: encapsulate Pp.message in Feedback.feedbackCarst Tankink
2014-06-25all coqide specific files moved into ide/Enrico Tassi
2014-06-07Moving a Thread.yield in check_interrupt.Pierre-Marie Pédrot
2014-06-07Adding a new Control file centralizing the control options of Coq.Pierre-Marie Pédrot
2014-05-06- Fix comparison of universes.Matthieu Sozeau
2014-04-08printer for coqchkEnrico Tassi
2014-03-05Adding a canary library. This canary is imperfect. It allows serializationPierre-Marie Pédrot
2014-03-05Added a new module HMap. It works (almost) like Map, except that it expectsPierre-Marie Pédrot
2014-03-05Adding a CSet module in Coq lib.Pierre-Marie Pédrot
2013-10-18Ephemeron: marshaling friendly keysgareuselesinge
2013-09-06Moving Searchstack to CStack, and normalizing names a bit.ppedrot
2013-08-25Added a more efficient way to recover the domain of a map.ppedrot
2013-08-20Fix compilation of coqcheckgareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-05-12Added a generic notion of hook. Hooks are functions to be setppedrot
2013-05-08Uniformizing the [if_warn] flag used for warning printing and putppedrot
2013-04-15Checker: vo validation is now done in check.ml (and always)letouzey
2013-04-15Checker: reified encoding of .vo types in values.mlletouzey
2013-03-13Fix compilation of coqchk (broken by commit 16268), bis repetitaletouzey
2013-03-13Fix compilation of coqchk (broken by commit 16268)letouzey
2013-02-18Added exception enrichment. Now one can define additional arbitraryppedrot
2013-01-28Added backtrace primitives.ppedrot
2012-12-14Moving hcons_string to String namespace.ppedrot
2012-11-13Added a CString module.ppedrot
2012-11-08Added an Int module with dummy utility functions.ppedrot
2012-10-04Getting rid of Compat in the checker.ppedrot
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
2012-09-26Reusing the Hashset data structure in Hashcons. Hopefully, this shouldppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:08:53 +0000