aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
Commit message (Expand)AuthorAge
* 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
| | * Univs: update checkerGravatar Matthieu Sozeau2015-10-02
| |/
| * Make the interface of System.raw_extern_intern much saner.Gravatar Guillaume Melquiond2015-09-29
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-09-06
|\|
| * Implementing Herbelin's fix for the "NonPar" bugGravatar mlasson2015-09-03
| * Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
| * Hconsing continuedGravatar Hugo Herbelin2015-08-02
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-07-18
|\|
| * Univs/Inductive: fix typechecking of casesGravatar Matthieu Sozeau2015-07-15
| * Updating checksum in checker (9c732a5cc continued).Gravatar Hugo Herbelin2015-07-12
| * Unused variables reported by OCaml.Gravatar Hugo Herbelin2015-07-10
| * Option -type-in-type: added support in checker and making it contaminatingGravatar Hugo Herbelin2015-07-10
| * Kernel/Checker: Cleanup fixes of substitutions due to let-ins.Gravatar Matthieu Sozeau2015-07-09
| * Template polymorphism: A bug-fix for Bug #4258Gravatar mlasson2015-07-09
| * Checker: Report bugfixes from kernel/inductive.mlGravatar Matthieu Sozeau2015-07-08
| * Checker: Fix bug #4282Gravatar Matthieu Sozeau2015-07-07