aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Expand)Author
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-28Refine Gregory Malecha's patch on VM and universe polymorphism.Maxime Dénès
2015-10-28Adds support for the virtual machine to perform reduction of universe polymor...Gregory Malecha
2015-10-27Type-safe Egramml.grammar_prod_item.Pierre-Marie Pédrot
2015-10-26Pcoq entries are given a proper module.Pierre-Marie Pédrot
2015-10-18Adding a notion of monotonous evarmap.Pierre-Marie Pédrot
2015-10-17Dedicated file for universe unification context manipulation.Pierre-Marie Pédrot
2015-10-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-14Reverting modifications in dev/top_printers pushed mistakenly.Pierre-Marie Pédrot
2015-10-14Fixing perfomance issue of auto hints induced by universes.Pierre-Marie Pédrot
2015-10-13Fix some typos.Guillaume Melquiond
2015-10-10Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-09Code cleaning in VM (with Benjamin).Maxime Dénès
2015-10-09Minor typo in universe polymorphism doc.Maxime Dénès
2015-10-06Splitting kernel universe code in two modules.Pierre-Marie Pédrot
2015-10-06Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Updating versions history with data from Gérard.Hugo Herbelin
2015-10-02Update the history of versions with recent versions.Hugo Herbelin
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Univs: More info for developers.Matthieu Sozeau
2015-09-20Better debug printers for module paths.Maxime Dénès
2015-09-17Merge branch 'v8.5' into trunkMaxime Dénès
2015-09-17Fix Windows installer.Guillaume Melquiond
2015-08-22Merge branch 'v8.5'Pierre-Marie Pédrot
2015-08-17windows build scripts made more accurate in detecting failuresEnrico Tassi
2015-08-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-30A printer for printing constants of the env (maybe useful when there are not ...Hugo Herbelin
2015-07-27Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-23adding a missing case for printing zippers.Gregory Malecha
2015-07-02Merge branch 'v8.5' into trunkMaxime Dénès
2015-06-29Assumptions: more informative print for False axiom (Close: #4054)Enrico Tassi
2015-06-29win: compile with -debugEnrico Tassi
2015-06-25Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Thomas Sibut-Pinote
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-01script to build 64 coq installer for windowsEnrico Tassi
2015-05-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-04-21Fixing #4198 (looking for subterms also in the return clause of match).Hugo Herbelin
2015-03-27use a more compact representation of non-constant constructorsBenjamin Gregoire
2015-03-26fix compilationBenjamin Gregoire
2015-02-27Adding a new folder corresponding to the low-level part of the pretyperPierre-Marie Pédrot
2015-02-19Adding a possible DEPRECATED flag to VERNAC EXTEND statements.Pierre-Marie Pédrot
2015-02-12Revert "Using same code for browsing physical directories in coqtop and coqdep."Hugo Herbelin
2015-02-12Using same code for browsing physical directories in coqtop and coqdep.Hugo Herbelin
2015-02-05Windows installer cleanupEnrico Tassi
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-15vm_printers: fix compilationEnrico Tassi
2015-01-12Update headers.Maxime Dénès
2015-01-08Avoiding introducing yet another convention in naming files.Hugo Herbelin