aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-05-20Adapt the documentation to the move from Gitter to Zulip.Théo Zimmermann
2020-05-20Merge PR #12359: [ci] Add mit-plv/engine-benchGaëtan Gilbert
2020-05-20[obligations] [nit] Refactor obligation printing.Emilio Jesus Gallego Arias
2020-05-20[obligations] `declare_obligation` now takes an `UState.t`Emilio Jesus Gallego Arias
2020-05-20[declare] [nit] Use proper type alias for in ProgramDecl interfaceEmilio Jesus Gallego Arias
2020-05-20[nit] Remove `Declare.Obls.err_not_transp`Emilio Jesus Gallego Arias
2020-05-20Merge PR #12350: [test-suite] Ensure copies of files are writableGaëtan Gilbert
2020-05-20Merge PR #12356: [declare] Remove unused parameters in prepare_obligationGaëtan Gilbert
2020-05-20Merge PR #12354: [universes] [api] Provide UState.from_envGaëtan Gilbert
2020-05-20Merge PR #12342: Direct URL for triggering a pipeline with SKIP_DOCKER=false.Gaëtan Gilbert
2020-05-20Bump nixpkgs to get ocamlformat 0.14.2.Théo Zimmermann
2020-05-20Merge PR #12362: Use dev version for opam git pinning in .gitlab-ci.yml.Emilio Jesus Gallego Arias
2020-05-19Delay evaluating arguments of the "exists" tacticAttila Gáspár
2020-05-19[ci] Add mit-plv/engine-benchJason Gross
2020-05-19[topfmt] Set formatter + flush fixEmilio Jesus Gallego Arias
2020-05-19[ci] [docker] Bump ocamlformat and duneEmilio Jesus Gallego Arias
2020-05-19Use dev version for opam git pinning in .gitlab-ci.yml.Théo Zimmermann
2020-05-19Merge PR #12224: Support :gdef:`text<term>` syntax (adding "<term>")Clément Pit-Claudel
2020-05-19[declare] Remove unused parameters in prepare_obligationEmilio Jesus Gallego Arias
2020-05-19[declare] Minor tweaks in prepare_obligationEmilio Jesus Gallego Arias
2020-05-19[declare] Remove dead code in prepare_obligationEmilio Jesus Gallego Arias
2020-05-19[universes] [api] Provide UState.from_envEmilio Jesus Gallego Arias
2020-05-19Merge PR #12353: Update release-process.mdEmilio Jesus Gallego Arias
2020-05-19Merge PR #12301: [declare] Grand unification of the proof save path.Gaëtan Gilbert
2020-05-19[primitive floats] Add low level hexadecimal printingPierre Roux
2020-05-18Use the new gdef alt-text feature in the refman.Théo Zimmermann
2020-05-18Support :gdef:`text <term>` syntax (adding "<term>")Jim Fehrle
2020-05-18Bump minimal versions of refman dependencies.Théo Zimmermann
2020-05-18[ci] Old overlay cleanup.Emilio Jesus Gallego Arias
2020-05-18[declare] Grand unification of the proof save path.Emilio Jesus Gallego Arias
2020-05-18[declare] Merge `DeclareObl` into `Declare`Emilio Jesus Gallego Arias
2020-05-18[obligations] Pre-functionalize Program stateEmilio Jesus Gallego Arias
2020-05-18Update release-process.mdEnrico Tassi
2020-05-18Update release-process.mdEnrico Tassi
2020-05-18Merge PR #12289: test-suite: fix bug causing unit tests to be skippedHugo Herbelin
2020-05-18[test-suite] Ensure copies of files are writableEmilio Jesus Gallego Arias
2020-05-18Merge PR #12346: Update to 8.13.Emilio Jesus Gallego Arias
2020-05-18Update to 8.13.Théo Zimmermann
2020-05-18Merge PR #11980: Improve spacing in Print AssumptionsEmilio Jesus Gallego Arias
2020-05-18Merge PR #12341: [search] [ssr] Emit deprecated message when calling search f...Théo Zimmermann
2020-05-18Direct URL for triggering a pipeline with SKIP_DOCKER=false.Théo Zimmermann
2020-05-18[azure OSX] Export OCAMLPATH so test-suite sees OCaml libsEmilio Jesus Gallego Arias
2020-05-18Merge PR #12345: test-suite/Makefile: fix incomplete prerequisite listEmilio Jesus Gallego Arias
2020-05-18[search] [ssr] Emit deprecated message when calling search from ssreflectEmilio Jesus Gallego Arias
2020-05-18Cleanup: remove noisy "uctx_" prefixes in ustate.mlGaëtan Gilbert
2020-05-18test-suite/Makefile: fix incomplete prerequisite listGaëtan Gilbert
2020-05-18Improve spacing in Print AssumptionsGaëtan Gilbert
2020-05-18Cleanup: remove noisy "sec_" prefixes in section.mlGaëtan Gilbert
2020-05-17Merge PR #11981: Ltac2: add notations for eval cbv in ... and other in place ...Jason Gross
2020-05-17Revert "[test] unit tests for ide/coq_lex.ml" + makefile supportGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 00:45:23 +0000