aboutsummaryrefslogtreecommitdiff
path: root/checker
AgeCommit message (Expand)Author
2016-07-25Fix bug #4876: critical bug in guard condition checker.Matthieu Sozeau
2016-06-23Remove extraction-specific code from the checker.Guillaume Melquiond
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-05-02Make votour a bit more robust/forgiving with respect to user commands (bug #4...Guillaume Melquiond
2016-04-28Fix missing newline in coqchk engagement (bug #4694).Guillaume Melquiond
2016-03-22A patch renaming equal into eq in the module dealing withHugo Herbelin
2016-03-04Rename Ephemeron -> CEphemeron.Maxime Dénès
2016-01-20Update cic.mli MD5 after header update.Maxime Dénès
2016-01-20Update copyright headers.Maxime Dénès
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-11-04Checker was forgetting to register global universes introduced by opaqueMatthieu Sozeau
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-03Implementing Herbelin's fix for the "NonPar" bugmlasson
2015-08-02Reverting 16 last commits, committed mistakenly using the wrong push command.Hugo Herbelin
2015-08-02Hconsing continuedHugo Herbelin
2015-07-15Univs/Inductive: fix typechecking of casesMatthieu Sozeau
2015-07-12Updating checksum in checker (9c732a5cc continued).Hugo Herbelin
2015-07-10Unused variables reported by OCaml.Hugo Herbelin
2015-07-10Option -type-in-type: added support in checker and making it contaminatingHugo Herbelin
2015-07-09Kernel/Checker: Cleanup fixes of substitutions due to let-ins.Matthieu Sozeau
2015-07-09Template polymorphism: A bug-fix for Bug #4258mlasson
2015-07-08Checker: Report bugfixes from kernel/inductive.mlMatthieu Sozeau
2015-07-07Checker: Fix bug #4282Matthieu Sozeau
2015-06-25Adding a more efficient representation of OCaml objects in votour.Pierre-Marie Pédrot
2015-06-25Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Thomas Sibut-Pinote
2015-06-24On-demand Require.Pierre-Marie Pédrot
2015-06-24Splitting the library representation on disk in two.Pierre-Marie Pédrot
2015-06-20Votour displays wordsize of segments before loading them.Pierre-Marie Pédrot
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-03-31Removing references to deprecated syntax -I/-R -as.Pierre-Marie Pédrot
2015-03-25Exporting memory representation of STM tasks for votour.Pierre-Marie Pédrot
2015-03-24Functorized interface over object representation in votour.Pierre-Marie Pédrot
2015-03-24Fixing representation of dynamics in votour (again).Pierre-Marie Pédrot
2015-03-23coqchk: more prints when -debugEnrico Tassi
2015-03-18Fixing internal representation of Dyn.t in votour.Pierre-Marie Pédrot
2015-03-02Now accepting unit props in mutual definitionsBruno Barras
2015-02-26Fix checker after addition of a universe context in with t := c constraints.Matthieu Sozeau
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
2015-02-11Fixing bug #4019, and checker blow-up at once.Pierre-Marie Pédrot
2015-02-11Clarifying the implementation of universe hashconsing.Pierre-Marie Pédrot
2015-02-05Windows: open .vo files in binary modeEnrico Tassi
2015-01-13Update hash of cic.mli in checker/values.ml,Matthieu Sozeau
2015-01-12Update headers.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 11:44:26 +0000