aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-03-14Merge PR #9700: [dune] [checker] Don't install internal checker library.Théo Zimmermann
2019-03-14Exposes Coq_micromega.dump_proof_term to allow a use independent from tacticsChantal Keller
2019-03-14Correct dependencies in the micromega packChantal Keller
2019-03-13Merge PR #9736: Don't coqchk the test suite prerequisitesEnrico Tassi
2019-03-13Merge PR #9757: [refman] Add 'warn' option to coqtop directive.Emilio Jesus Gallego Arias
2019-03-13Merge PR #9723: Fix undefined gramlib_MLLIB_DEPENDENCIES in make installEnrico Tassi
2019-03-13Merge PR #9739: [dune] [configure] Fix `gramlib` path for hardcoded includes.Enrico Tassi
2019-03-13Merge PR #9748: [dune] Add shim for coqtop.byteThéo Zimmermann
2019-03-13[refman] Fix Sphinx-translation regression in Arguments command.Théo Zimmermann
2019-03-13[refman] Remove warning silencing by fixing the underlying issue.Théo Zimmermann
2019-03-13[refman] Fix other newly emitted warnings.Théo Zimmermann
2019-03-13Merge PR #9627: Small retroknowledge/primitive cleanupVincent Laporte
2019-03-12[refman] Add 'warn' option to coqtop directive.Théo Zimmermann
2019-03-12Merge PR #9632: Fix #9631: Instance: anomaly grounding non evar-free termEmilio Jesus Gallego Arias
2019-03-12Merge PR #9596: Fix #9595: missing non-primitive-record warning with 0 field ...Emilio Jesus Gallego Arias
2019-03-12Merge PR #9389: Implement a method for manual declaration of implicits.Emilio Jesus Gallego Arias
2019-03-12Merge PR #7819: Ho matching occ selEnrico Tassi
2019-03-12[dune] Add shim for coqtop.byteEmilio Jesus Gallego Arias
2019-03-12Merge PR #9738: [ci] [docker] Upgrade odoc to 1.4.0Gaëtan Gilbert
2019-03-11Make NotConvertibleVect exception internal to typeopsGaëtan Gilbert
2019-03-11[dune] [configure] Fix `gramlib` path for hardcoded includes.Emilio Jesus Gallego Arias
2019-03-11[ci] [docker] Upgrade odoc to 1.4.0Emilio Jesus Gallego Arias
2019-03-11Don't coqchk the test suite prerequisitesGaëtan Gilbert
2019-03-11Fix undefined gramlib_MLLIB_DEPENDENCIES in make installGaëtan Gilbert
2019-03-11Nicer error for bad primitive types (through type_errors etc)Gaëtan Gilbert
2019-03-11Remove unused Retroknowledge.Register_inlineGaëtan Gilbert
2019-03-11Merge PR #9698: Remove last random failuresGaëtan Gilbert
2019-03-11Merge PR #9675: Dune: remove -short-paths flag.Emilio Jesus Gallego Arias
2019-03-11Merge PR #9570: Refresh contributing guide and README.Maxime Dénès
2019-03-10Merge PR #9654: [sphinx] Add warn option to coqtop directive.Clément Pit-Claudel
2019-03-10Merge PR #9728: Fix issue #9722 pkg-config not foundThéo Zimmermann
2019-03-08Fix issue #9722 pkg-config not foundMichael Soegtrop
2019-03-08Merge PR #9720: [refman] Fix typo in local application of tacticsThéo Zimmermann
2019-03-08[sphinx] Fix typo in local application of tacticshawnzug
2019-03-07Merge PR #9133: Move README-V1-V5 to credits chapterClément Pit-Claudel
2019-03-06Merge PR #9476: Constructor type information uses the expanded form.Gaëtan Gilbert
2019-03-05Merge PR #9524: Fix #7632: Change syntax of autoapply according to the docume...Pierre-Marie Pédrot
2019-03-05Merge PR #9701: [CI] Add stdlib2Emilio Jesus Gallego Arias
2019-03-05[CI] Add stdlib2Vincent Laporte
2019-03-05[dune] [checker] Don't install internal checker library.Emilio Jesus Gallego Arias
2019-03-05Remove regularly failing test from test-suite.Théo Zimmermann
2019-03-05Put regularly failing async tests in allow_failure mode.Théo Zimmermann
2019-03-05[make] Sphinx: install only `html/` and `latex/` directoriesVincent Laporte
2019-03-04Merge PR #9687: Cleanup exported variables in Makefile.buildEnrico Tassi
2019-03-04remove unused import of osFrédéric Chapoton
2019-03-04Merge PR #8700: Removing debugging warning when no exception handler is regis...Emilio Jesus Gallego Arias
2019-03-04Merge PR #9688: [stm] unfocus when edition exits the proof (fix #9431)Emilio Jesus Gallego Arias
2019-03-04[dune] [ide] Don't install the internal CoqIDE UI library.Emilio Jesus Gallego Arias
2019-03-04Removing debugging warning when no exception handler is registered in futures.Hugo Herbelin
2019-03-04Merge PR #9660: Set COQLIB so the test suite runs locally on Windows.Enrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 21:51:09 +0000