aboutsummaryrefslogtreecommitdiff
path: root/checker
AgeCommit message (Expand)Author
2016-07-26Merge remote-tracking branch 'gforge/v8.5' into v8.6Matthieu Sozeau
2016-07-25Fix bug #4876: critical bug in guard condition checker.Matthieu Sozeau
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-06-27Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-23Remove extraction-specific code from the checker.Guillaume Melquiond
2016-06-18Fixing the checker.Pierre-Marie Pédrot
2016-06-16Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Pierre-Marie Pédrot
2016-06-16Fixing the checker.Pierre-Marie Pédrot
2016-06-14Preventive compatibility fixes for flushing.Emilio Jesus Gallego Arias
2016-06-14configure: use ln on linux and cp on windowsEnrico Tassi
2016-06-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-07Do not use COQLIBS for the validate rule produced by coq_makefile (bug #4693).Guillaume Melquiond
2016-06-05Fix incorrect checking of library checksums.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-05-31Checker: avoid using obsolete names from NamesPierre Letouzey
2016-05-31Checker: no more -I kernel via a few symlinks (for Names and Esubst)Pierre Letouzey
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-02Make votour a bit more robust/forgiving with respect to user commands (bug #4...Guillaume Melquiond
2016-05-02Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-28Fix missing newline in coqchk engagement (bug #4694).Guillaume Melquiond
2016-03-30Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-22A patch renaming equal into eq in the module dealing withHugo Herbelin
2016-03-10Removing OCaml deprecated function names from the Lazy module.Pierre-Marie Pédrot
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-04Rename Ephemeron -> CEphemeron.Maxime Dénès
2016-02-15CLEANUP: Simplifying the changes done in "checker/*"Matej Kosik
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update cic.mli MD5 after header update.Maxime Dénès
2016-01-20Update copyright headers.Maxime Dénès
2016-01-06Remove deprecated command-line options such as "-as".Guillaume Melquiond
2016-01-06Merge remote-tracking branch 'origin/v8.5' into trunkGuillaume Melquiond
2016-01-06Protect code against changes in Map interface.Maxime Dénès
2016-01-05Fix order of files in mllib.Maxime Dénès
2015-12-31Remove unused function Checker.print_loc.Guillaume Melquiond
2015-12-22Do not compose "str" and "to_string" whenever possible.Guillaume Melquiond
2015-12-05Factorizing unsafe code by relying on the new Dyn module.Pierre-Marie Pédrot
2015-11-15Displaying the object identifier in votour.Pierre-Marie Pédrot
2015-11-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-04Checker was forgetting to register global universes introduced by opaqueMatthieu Sozeau
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Univs: fix checker generating undeclared universes.Matthieu Sozeau
2015-10-02Univs: update checkerMatthieu Sozeau
2015-09-29Make the interface of System.raw_extern_intern much saner.Guillaume Melquiond
2015-09-06Merge branch 'v8.5'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:57:12 +0000