aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
Commit message (Expand)AuthorAge
* Merge remote-tracking branch 'github/pr/257' into v8.6Gravatar Maxime Dénès2016-09-30
|\
* | fix bug 3683 : adds references to the web site for the bug trackerGravatar Yves Bertot2016-09-29
| * [checker] Fix/fine tune printing.Gravatar Emilio Jesus Gallego Arias2016-08-18
|/
* Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-07-26
|\
| * Fix bug #4876: critical bug in guard condition checker.Gravatar Matthieu Sozeau2016-07-25
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* | Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* | A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-27
|\|
| * Remove extraction-specific code from the checker.Gravatar Guillaume Melquiond2016-06-23
* | Fixing the checker.Gravatar Pierre-Marie Pédrot2016-06-18
* | Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \
| * | Fixing the checker.Gravatar Pierre-Marie Pédrot2016-06-16
* | | Preventive compatibility fixes for flushing.Gravatar Emilio Jesus Gallego Arias2016-06-14
* | | configure: use ln on linux and cp on windowsGravatar Enrico Tassi2016-06-14
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-09
|\ \ \ | | |/ | |/|
| * | Do not use COQLIBS for the validate rule produced by coq_makefile (bug #4693).Gravatar Guillaume Melquiond2016-06-07
| * | Fix incorrect checking of library checksums.Gravatar Maxime Dénès2016-06-05
* | | Merge branch 'yet-another-makefile-bigbang' into trunkGravatar Pierre Letouzey2016-06-01
|\ \ \
| * | | Makefile: restore the use of coqdep_boot for creating .v.d filesGravatar Pierre Letouzey2016-06-01
* | | | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
|/ / /
* | | Checker: avoid using obsolete names from NamesGravatar Pierre Letouzey2016-05-31
* | | Checker: no more -I kernel via a few symlinks (for Names and Esubst)Gravatar Pierre Letouzey2016-05-31
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\| |
| * | Make votour a bit more robust/forgiving with respect to user commands (bug #4...Gravatar Guillaume Melquiond2016-05-02
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-02
|\| |
| * | Fix missing newline in coqchk engagement (bug #4694).Gravatar Guillaume Melquiond2016-04-28
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-30
|\| |
| * | A patch renaming equal into eq in the module dealing withGravatar Hugo Herbelin2016-03-22
* | | Removing OCaml deprecated function names from the Lazy module.Gravatar Pierre-Marie Pédrot2016-03-10
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-05
|\| |
| * | Rename Ephemeron -> CEphemeron.Gravatar Maxime Dénès2016-03-04
* | | CLEANUP: Simplifying the changes done in "checker/*"Gravatar Matej Kosik2016-02-15
* | | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\| |
| * | Update cic.mli MD5 after header update.Gravatar Maxime Dénès2016-01-20
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | | Remove deprecated command-line options such as "-as".Gravatar Guillaume Melquiond2016-01-06
* | | Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Guillaume Melquiond2016-01-06
|\| |
| * | Protect code against changes in Map interface.Gravatar Maxime Dénès2016-01-06
| * | Fix order of files in mllib.Gravatar Maxime Dénès2016-01-05
* | | Remove unused function Checker.print_loc.Gravatar Guillaume Melquiond2015-12-31
* | | Do not compose "str" and "to_string" whenever possible.Gravatar Guillaume Melquiond2015-12-22
* | | Factorizing unsafe code by relying on the new Dyn module.Gravatar Pierre-Marie Pédrot2015-12-05
* | | Displaying the object identifier in votour.Gravatar Pierre-Marie Pédrot2015-11-15
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-05
|\| |
| * | Checker was forgetting to register global universes introduced by opaqueGravatar Matthieu Sozeau2015-11-04
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\| |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\ \ \
| | * | Univs: fix checker generating undeclared universes.Gravatar Matthieu Sozeau2015-10-02