aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
Commit message (Expand)AuthorAge
* Checker was forgetting to register global universes introduced by opaqueGravatar Matthieu Sozeau2015-11-04
* 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
* 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
* 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
* Adding a more efficient representation of OCaml objects in votour.Gravatar Pierre-Marie Pédrot2015-06-25
* Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Gravatar Thomas Sibut-Pinote2015-06-25
* On-demand Require.Gravatar Pierre-Marie Pédrot2015-06-24
* Splitting the library representation on disk in two.Gravatar Pierre-Marie Pédrot2015-06-24
* Votour displays wordsize of segments before loading them.Gravatar Pierre-Marie Pédrot2015-06-20
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Removing references to deprecated syntax -I/-R -as.Gravatar Pierre-Marie Pédrot2015-03-31
* Exporting memory representation of STM tasks for votour.Gravatar Pierre-Marie Pédrot2015-03-25
* Functorized interface over object representation in votour.Gravatar Pierre-Marie Pédrot2015-03-24
* Fixing representation of dynamics in votour (again).Gravatar Pierre-Marie Pédrot2015-03-24
* coqchk: more prints when -debugGravatar Enrico Tassi2015-03-23
* Fixing internal representation of Dyn.t in votour.Gravatar Pierre-Marie Pédrot2015-03-18
* Now accepting unit props in mutual definitionsGravatar Bruno Barras2015-03-02
* Fix checker after addition of a universe context in with t := c constraints.Gravatar Matthieu Sozeau2015-02-26
* Revert "Using same code for browsing physical directories in coqtop and coqdep."Gravatar Hugo Herbelin2015-02-12
* Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)Gravatar Hugo Herbelin2015-02-12
* Capital letter in plugins.Gravatar Hugo Herbelin2015-02-12
* Using same code for browsing physical directories in coqtop and coqdep.Gravatar Hugo Herbelin2015-02-12
* Fixing bug #4019, and checker blow-up at once.Gravatar Pierre-Marie Pédrot2015-02-11
* Clarifying the implementation of universe hashconsing.Gravatar Pierre-Marie Pédrot2015-02-11
* Windows: open .vo files in binary modeGravatar Enrico Tassi2015-02-05
* Update hash of cic.mli in checker/values.ml,Gravatar Matthieu Sozeau2015-01-13
* Update headers.Gravatar Maxime Dénès2015-01-12
* Declarations.mli refactoring: module_type_body = module_bodyGravatar Pierre Letouzey2015-01-11
* Fix checker's treatment of template polymorphicGravatar Matthieu Sozeau2015-01-06
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
* updated include file for debuggingGravatar Bruno Barras2015-01-06
* improve efficiency of the reduction interpreter of the checkerGravatar Bruno Barras2015-01-06
* coqchk: flush the pp buffer from time to timeGravatar Enrico Tassi2014-12-26
* Vi2vo: fix handling of univ constraints coming from the bodyGravatar Enrico Tassi2014-12-23
* Fixing performance issue of checker validation.Gravatar Pierre-Marie Pédrot2014-12-19
* Fixing checker representation of values.Gravatar Pierre-Marie Pédrot2014-12-19
* update md5 sums to make "make check" workGravatar Enrico Tassi2014-12-19
* Fix sigsegv in checkerGravatar Enrico Tassi2014-12-19
* Fixing checker representation of universe lists.Gravatar Pierre-Marie Pédrot2014-12-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 21:35:35 +0000