aboutsummaryrefslogtreecommitdiff
path: root/checker
AgeCommit message (Expand)Author
2015-06-25Adjust checker after `Assume [Positive]`.Arnaud Spiwack
2015-06-24Merge branch 'v8.5'Pierre-Marie Pédrot
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-23Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Thomas Sibut-Pinote
2015-06-22Merge remote-tracking branch 'forge/v8.5'Pierre Boutillier
2015-06-20Votour displays wordsize of segments before loading them.Pierre-Marie Pédrot
2015-05-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-04-09Merge branch 'v8.5' into trunkPierre Letouzey
2015-03-31Removing references to deprecated syntax -I/-R -as.Pierre-Marie Pédrot
2015-03-30Merge branch 'v8.5' into trunkEnrico Tassi
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-23Merge branch 'v8.5'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-03-02Now accepting unit props in mutual definitionsBruno Barras
2015-02-26Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-26Fix checker after addition of a universe context in with t := c constraints.Matthieu Sozeau
2015-02-16Using same code for browsing physical directories in coqtop and coqdep.Hugo Herbelin
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
2015-01-11Declarations.mli refactoring: module_type_body = module_bodyPierre Letouzey
2015-01-06Fix checker's treatment of template polymorphicMatthieu Sozeau
2015-01-06rename: vi -> vioEnrico Tassi
2015-01-06updated include file for debuggingBruno Barras
2015-01-06improve efficiency of the reduction interpreter of the checkerBruno Barras
2014-12-26coqchk: flush the pp buffer from time to timeEnrico Tassi
2014-12-23Vi2vo: fix handling of univ constraints coming from the bodyEnrico Tassi
2014-12-19Fixing performance issue of checker validation.Pierre-Marie Pédrot
2014-12-19Fixing checker representation of values.Pierre-Marie Pédrot
2014-12-19update md5 sums to make "make check" workEnrico Tassi
2014-12-19Fix sigsegv in checkerEnrico Tassi
2014-12-18Fixing checker representation of universe lists.Pierre-Marie Pédrot
2014-12-18Backporting the change in lists of universes to the checker.Pierre-Marie Pédrot
2014-12-17checker: Change in library on disk values, now using context_sets instead ofMatthieu Sozeau
2014-12-17Ensuring the good invariants of hashcons table generation in the API.Pierre-Marie Pédrot
2014-12-17Update checker/values and cic due to changes in case_info and record_body.Matthieu Sozeau
2014-11-14Exit with code 129 when an anomaly occurs.Xavier Clerc
2014-10-20A patch for printing "match" when constructors are defined with let-inHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 09:07:31 +0000