aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-04-25Merge Ltac2 pluginMaxime Dénès
2019-04-25Prepare merge into CoqMaxime Dénès
2019-04-23Merge PR #9962: [native compiler] Encoding of constructors based on tagsPierre-Marie Pédrot
2019-04-23Merge PR #9889: Fix pretty-printing of primitive integersMaxime Dénès
2019-04-23Merge PR #9978: Remove duplicate copy of _warn_if_duplicate_name.Gaëtan Gilbert
2019-04-23Merge PR #9973: update elpi to version 1.2Gaëtan Gilbert
2019-04-21Remove duplicate copy of _warn_if_duplicate_name.Jim Fehrle
2019-04-20Merge PR #9836: [schemes] Don't re-declare scheme side-effects that are alrea...Enrico Tassi
2019-04-20Merge PR #9906: coq_makefile install target: error if any file is missingEnrico Tassi
2019-04-20overlay for elpiEnrico Tassi
2019-04-20update elpi to version 1.2Enrico Tassi
2019-04-17Merge PR #9966: Add changes for -setEmilio Jesus Gallego Arias
2019-04-17Add changes for -setGaëtan Gilbert
2019-04-17Merge PR #9876: Command-line setters for optionsEmilio Jesus Gallego Arias
2019-04-17Merge PR #9891: [CI] Build CoqIDE for macOS on AzurePierre-Marie Pédrot
2019-04-16Merge PR #9165: Recarg cleanupEmilio Jesus Gallego Arias
2019-04-16Merge PR #9898: Better error message when OCaml compiler not found for native...Emilio Jesus Gallego Arias
2019-04-16[doc] [kernel] Add docstrings for native interface functions.Emilio Jesus Gallego Arias
2019-04-16Better error message when OCaml compiler not found for native computeMaxime Dénès
2019-04-16[doc] Changes for coq/coq#9165Emilio Jesus Gallego Arias
2019-04-16[ci] Overlays for coq/coq#9165Emilio Jesus Gallego Arias
2019-04-16[ast] [constrexpr] Make recursion_order_expr an AST node.Emilio Jesus Gallego Arias
2019-04-16Update and fix documentation of Program Fixpoint with measureMaxime Dénès
2019-04-16Fix spurious argument of {measure}Maxime Dénès
2019-04-16Take advantage of relaxed {measure} syntax in test suiteMaxime Dénès
2019-04-16Clean the representation of recursive annotation in ConstrexprMaxime Dénès
2019-04-16Command-line setters for optionsGaëtan Gilbert
2019-04-16[CI/Azure/macOS] Set MACOSX_DEPLOYMENT_TARGET to 10.12Vincent Laporte
2019-04-16[CI/Azure/macOS] Install Coq into an artifactVincent Laporte
2019-04-15[native compiler] Encoding of constructors based on tagsMaxime Dénès
2019-04-15[native compiler] Remove unused universe argument in LmakeblockMaxime Dénès
2019-04-15[native compiler] Distinguish constant constructors in lambda codeMaxime Dénès
2019-04-15[CI/Azure/macOS] Build CoqIDEVincent Laporte
2019-04-15[CoqIDE] Fix build system for macOSVincent Laporte
2019-04-15[CI] Print test-suite log on failure (macOS/Azure)Vincent Laporte
2019-04-15Merge PR #9927: Don't store closures in summary (reduction effects)Pierre-Marie Pédrot
2019-04-15Merge PR #9959: [native compiler] Remove `Lconstruct` from lambda code.Pierre-Marie Pédrot
2019-04-14[native compiler] Remove now unused GconstructMaxime Dénès
2019-04-14[native compiler] Remove `Lconstruct` from lambda code.Maxime Dénès
2019-04-14Merge PR #9957: Add missing build dependency in `coq.opam`Emilio Jesus Gallego Arias
2019-04-14Fix coq/coq#9956Erik Martin-Dorel
2019-04-12Merge PR #9949: [stm] Report correct ids on some errors where it was dummy.Enrico Tassi
2019-04-12Unify Set and Unset handling for optionsGaëtan Gilbert
2019-04-11[stm] Report correct ids on some errors where it was dummy.Shachar Itzhaky
2019-04-11Merge pull request coq/ltac2#119 from maximedenes/pretyping-rm-globalPierre-Marie Pédrot
2019-04-11Merge PR #9909: Remove all but one call to `Global` in the pretyperPierre-Marie Pédrot
2019-04-11Merge PR #9938: [coqdep] Exit with error code on exception.Pierre-Marie Pédrot
2019-04-10Merge PR #9943: [mailmap] Tweak Emilio's entries.Théo Zimmermann
2019-04-10Merge PR #9910: [api] [proofs] Remove dependency of proofs on interp.Gaëtan Gilbert
2019-04-10Overlays for Global removal in pretyperMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 19:10:40 +0000