aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
Commit message (Expand)AuthorAge
...
| * Removing references to deprecated syntax -I/-R -as.Gravatar Pierre-Marie Pédrot2015-03-31
* | Merge branch 'v8.5' into trunkGravatar Enrico Tassi2015-03-30
|\|
| * 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
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-03-23
|\|
| * 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
* | Now accepting unit props in mutual definitionsGravatar Bruno Barras2015-03-02
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-02-26
|\|
| * Fix checker after addition of a universe context in with t := c constraints.Gravatar Matthieu Sozeau2015-02-26
* | Using same code for browsing physical directories in coqtop and coqdep.Gravatar Hugo Herbelin2015-02-16
| * 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
* Backporting the change in lists of universes to the checker.Gravatar Pierre-Marie Pédrot2014-12-18
* checker: Change in library on disk values, now using context_sets instead ofGravatar Matthieu Sozeau2014-12-17
* Ensuring the good invariants of hashcons table generation in the API.Gravatar Pierre-Marie Pédrot2014-12-17
* Update checker/values and cic due to changes in case_info and record_body.Gravatar Matthieu Sozeau2014-12-17
* Exit with code 129 when an anomaly occurs.Gravatar Xavier Clerc2014-11-14
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
* Remove debug printing codeGravatar Matthieu Sozeau2014-09-06
* Cleanup code for looking up projection bodies.Gravatar Matthieu Sozeau2014-09-06
* Fix checker to handle projections with eta and universe polymorphism correctly,Gravatar Matthieu Sozeau2014-09-06
* Fix checker to handle projections with eta and universe polymorphism correctly.Gravatar Matthieu Sozeau2014-09-06
* Fix checking of constants in checker. Prelude can now be checked.Gravatar Matthieu Sozeau2014-09-06
* Remove unused substitution functions in checker.Gravatar Matthieu Sozeau2014-09-05
* Fix checker treatment of inductives using subst_instances instead of subst_un...Gravatar Matthieu Sozeau2014-09-05
* Fix checker/values.ml with latest changes due to projections and universes.Gravatar Matthieu Sozeau2014-09-05
* Rename eta_expand_ind_stacks, fix the one from the checker and adaptGravatar Matthieu Sozeau2014-09-05
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 14:42:22 +0000