aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* remove obsolete file dev/Makefile.ougGravatar Pierre Letouzey2017-02-17
* Merge PR#403: Split Vernacular Processing from ToplevelGravatar Maxime Dénès2017-02-16
|\
* \ Merge PR#431Gravatar Maxime Dénès2017-02-16
|\ \
| * | [travis] [External CI] CompCert official 8.6 support + UniMathGravatar Emilio Jesus Gallego Arias2017-02-15
| * | [travis] [External CI] Factor out math-comp installs.Gravatar Emilio Jesus Gallego Arias2017-02-15
| | * Make Obligations see fix_exnGravatar Enrico Tassi2017-02-15
| | * [stm] Remove unused legacy stm interface.Gravatar Emilio Jesus Gallego Arias2017-02-15
| | * [cosmetic] Reorder makefile as suggested by @herbelinGravatar Emilio Jesus Gallego Arias2017-02-15
| | * [stm] Reenable Show Script command.Gravatar Emilio Jesus Gallego Arias2017-02-15
| | * [stm] Break stm/toplevel dependency loop.Gravatar Emilio Jesus Gallego Arias2017-02-15
| |/ |/|
* | Merge PR#314: Miscellaneous fixes for Ocaml warnings.Gravatar Maxime Dénès2017-02-15
|\|
| * [unicode] Address comments in PR#314.Gravatar Emilio Jesus Gallego Arias2017-02-15
| * [safe-string] Switch to buffer to `Bytes`Gravatar Emilio Jesus Gallego Arias2017-02-14
| * [safe-string] Use `String.init` to build string.Gravatar Emilio Jesus Gallego Arias2017-02-14
| * [misc] Remove unused binding.Gravatar Emilio Jesus Gallego Arias2017-02-14
|/
* Merge PR#253: Sort Search results by relevanceGravatar Maxime Dénès2017-02-14
|\
| * Test-suite: output of SearchGravatar Arnaud Spiwack2017-02-14
* | Merge PR#349: Proofview: tclINDEPENDENTLGravatar Maxime Dénès2017-02-13
|\ \
| * | Proofview: tclINDEPENDENTLGravatar Enrico Tassi2017-02-10
|/ /
* | Merge PR#405: Type cleanup in `Metasyntax`Gravatar Maxime Dénès2017-02-08
|\ \
* \ \ Merge PR#393: Replace Typeops with Fast_typeopsGravatar Maxime Dénès2017-02-08
|\ \ \
* | | | Revert "Extraction: avoid deprecated functions of module String"Gravatar Pierre Letouzey2017-02-07
* | | | Extraction cosmetic: no whitespaces in printing empty modulesGravatar Pierre Letouzey2017-02-07
* | | | Extraction: remove the "print to devnull" hack now that pp isn't lazy anymoreGravatar Pierre Letouzey2017-02-07
* | | | Extraction: avoid deprecated functions of module StringGravatar Pierre Letouzey2017-02-07
* | | | Extraction: simplify the generated code for difficult name conflictsGravatar Pierre Letouzey2017-02-07
* | | | Extraction : get_duplicates (via option) instead of check_duplicates (via Not...Gravatar Pierre Letouzey2017-02-07
* | | | configure: avoid deprecated warningsGravatar Pierre Letouzey2017-02-07
* | | | Extraction: fix complexity issue #5310Gravatar Pierre Letouzey2017-02-07
* | | | Merge PR#425: [travis] [External CI] [geocoq] don't build slow fileGravatar Maxime Dénès2017-02-07
|\ \ \ \
| * | | | [travis] [External CI] [geocoq] don't build slow fileGravatar Emilio Jesus Gallego Arias2017-02-07
* | | | | Merge PR#424: [travis] [External CI] iris-coq: fix dependenciesGravatar Maxime Dénès2017-02-07
|\ \ \ \ \
| * | | | | [travis] [External CI] iris-coq: fix dependenciesGravatar Emilio Jesus Gallego Arias2017-02-07
|/ / / / /
| | | * / Type cleanup in `Metasyntax`Gravatar Emilio Jesus Gallego Arias2017-02-07
| |_|/ / |/| | |
* | | | Merge PR#421: [travis] Perform parallel testingGravatar Maxime Dénès2017-02-07
|\| | |
| * | | [travis] [External CI] GeoCoqGravatar Emilio Jesus Gallego Arias2017-02-07
| * | | [travis] Enable 32bit test-suite + validate.Gravatar Emilio Jesus Gallego Arias2017-02-07
| * | | [travis] Move ci files from `tools` to `dev`.Gravatar Maxime Dénès2017-02-07
| * | | [travis] [External CI] C-Corn color coquelicot cpdt fiat-crypto floqc iris-co...Gravatar Emilio Jesus Gallego Arias2017-02-07
| * | | [travis] [External CI] Script renaming.Gravatar Emilio Jesus Gallego Arias2017-02-07
| * | | [travis] Improvements to main scriptGravatar Emilio Jesus Gallego Arias2017-02-07
| * | | [travis] [External CI] compcert HoTT math-compGravatar Emilio Jesus Gallego Arias2017-02-07
| * | | [travis] Run tests using a parallel matrix.Gravatar Emilio Jesus Gallego Arias2017-02-06
|/ / /
* | | Merge PR#419: [travis] CoqIde + doc + last available LSTGravatar Maxime Dénès2017-02-06
|\ \ \
| * | | [travis] : more apt deps + parallel jobs + non-container basedGravatar Pierre-Yves Strub2017-02-04
| * | | [travis] CoqIde + doc + last available LSTGravatar Pierre-Yves Strub2017-02-04
|/ / /
* | | Merge PR#418: Travis CI configurationGravatar Maxime Dénès2017-02-03
|\ \ \
| * | | Travis CI configuration. Runs validate & test-suite.Gravatar Pierre-Yves Strub2017-02-03
|/ / /
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-01
|\ \ \
| * \ \ Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2017-02-01
| |\ \ \