aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-07-26More precise type for universe entries.Pierre-Marie Pédrot
2017-07-26Merge PR #905: [api] Remove type equalities from API.Maxime Dénès
2017-07-26Merge PR #857: Extraction: various fixes related with bug 4720Maxime Dénès
2017-07-26Merge PR #859: Extraction TestCompileMaxime Dénès
2017-07-26Merge PR #808: [api] Put some order in API.mliMaxime Dénès
2017-07-26Merge PR #750: Remove deprecated options of ./configure in 8.8Maxime Dénès
2017-07-26make sure that API-leaks cannot be reintroduced by mistakeMatej Košík
2017-07-25Makefile.ide: restore a coqide-binaries rule (fix bug 5667)Pierre Letouzey
2017-07-25[api] Remove type equalities from API.Emilio Jesus Gallego Arias
2017-07-25[api] Put modules in order in API.{mli,ml}Emilio Jesus Gallego Arias
2017-07-21Merge PR #897: Fix test suite on windows (wrt fake_ide and coq-makefile)Maxime Dénès
2017-07-21PMP sold us a Timeout on Windows with 1s resolution. Trying to improve it.Maxime Dénès
2017-07-21Install time command under Cygwin (required for timing scripts).Maxime Dénès
2017-07-20Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720)Pierre Letouzey
2017-07-20Merge PR #892: Improve do_split option of typeclass resolutionMaxime Dénès
2017-07-20fake_ide: do as coqide to find out coqtop pathEnrico Tassi
2017-07-20coq_makefile: use System.exists_dir for better portabilityEnrico Tassi
2017-07-20Windows: Sys.is_dir "foo/" always says no (so we strip trailing slash)Enrico Tassi
2017-07-20coq-makefile: strip windows drive letter when DESTDIR is not emptyEnrico Tassi
2017-07-20coq-makefile: treat coq_makefile as any other coq binaryEnrico Tassi
2017-07-20more verbose logs for coq-makefileEnrico Tassi
2017-07-20coq-makefile: quote using ' to preserve \ (windows paths)Enrico Tassi
2017-07-20coq-makefile: make test suite detect more errorsEnrico Tassi
2017-07-20In fake_ide, call coqtop.exe instead of coqtop on Win32.Maxime Dénès
2017-07-20Avoid using unsupported signals under Windows in fake_ide.Maxime Dénès
2017-07-20Remove trailing CR before diff in output and misc tests.Maxime Dénès
2017-07-20Print failure logs on appveyor.Maxime Dénès
2017-07-20Remove non-terminating Timeout tests from Hints.v.Maxime Dénès
2017-07-20Make coqlib relative in test suite (revert 024a7ab20b0)Maxime Dénès
2017-07-20Add AppVeyor infrastructure, launching the test suite under Windows.Maxime Dénès
2017-07-20Merge PR #900: [proofs] Remove circular dependency from Proofview to Goal.Maxime Dénès
2017-07-20Merge PR #899: [general] Move files to directories so they match linking order.Maxime Dénès
2017-07-20Merge PR #903: Documenting the purity / marshallability invariant of persiste...Maxime Dénès
2017-07-20Documenting the purity / marshallability invariant of persistent states.Pierre-Marie Pédrot
2017-07-20Merge PR #898: [pp] Fix bugs 5651 [incorrect thunk in pretty printer]Maxime Dénès
2017-07-20Merge PR #896: Prepare De Bruijn universe abstractions, Spin-off: CheckerMaxime Dénès
2017-07-20Merge PR #869: Enforce alternating separators in typeclass debug outputMaxime Dénès
2017-07-20Merge PR #877: Travis+4.05.0Maxime Dénès
2017-07-20Merge branch 'v8.7'Maxime Dénès
2017-07-19Merge PR #745: Add timing scriptsMaxime Dénès
2017-07-19Merge PR #855: Deprecate options that were introduced for compatibility with ...Maxime Dénès
2017-07-19Merge PR #770: [proof] Move bullets to their own module.Maxime Dénès
2017-07-19[proofs] Remove circular dependency from Proofview to Goal.Emilio Jesus Gallego Arias
2017-07-19[general] Move files to directories matching linking order.Emilio Jesus Gallego Arias
2017-07-19Merge PR #788: [API] Remove `open API` in ml files in favor of `-open API` flag.Maxime Dénès
2017-07-19[pp] Fix bugs 5651 [incorrect thunk in pretty printer]Emilio Jesus Gallego Arias
2017-07-19Fixing the checker w.r.t. wrongly used abstract universe contexts.Pierre-Marie Pédrot
2017-07-19Merge PR #895: [ci] VST is now built with IGNORECOQVERSION=true.Maxime Dénès
2017-07-18Improve do_split option of typeclass resolutionMatthieu Sozeau
2017-07-18[ci] VST is now built with IGNORECOQVERSION=true.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 16:07:20 +0000