aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
Commit message (Expand)AuthorAge
* 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
* 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
* Port last changes of the guard condition to checker.Gravatar Maxime Dénès2014-08-06
* STM: encapsulate Pp.message in Feedback.feedbackGravatar Carst Tankink2014-08-04
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
* Porting guard fix to checker.Gravatar Maxime Dénès2014-07-22
* Cleanup substitution inside universe instances, only done through subst_fn now,Gravatar Matthieu Sozeau2014-07-21
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
* Removing dead code in checker/univ.ml.Gravatar Pierre-Marie Pédrot2014-06-10
* Removing explanations of universe inconsistencies from the checker. TheyGravatar Pierre-Marie Pédrot2014-06-10
* Providing the checker with its own version of the Univ file.Gravatar Pierre-Marie Pédrot2014-06-10
* Removing 'open Univ' from checker.Gravatar Pierre-Marie Pédrot2014-06-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 00:41:23 +0000