aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-01-15Merge PR #11401: [nix] Dune-2 and other improvementsThéo Zimmermann
2020-01-15[Nix] Fix setup hook when COQPATH is not boundVincent Laporte
2020-01-15[Nix] Update reference to nixpkgsVincent Laporte
2020-01-15[Nix/CI] Add verdi-raftVincent Laporte
2020-01-15[Nix/CI] Update fiat_cryptoVincent Laporte
2020-01-14Merge PR #11370: [zify] elim let in MLPierre-Marie Pédrot
2020-01-14Merge PR #11249: [stdlib] Additional statements in List.vHugo Herbelin
2020-01-14Merge PR #11394: [coqdoc] Fix #11353: coqdoc -g omits all sentences with deco...Hugo Herbelin
2020-01-14[zify] elim let in MLFrédéric Besson
2020-01-14infercumulativity: take less argumentsGaëtan Gilbert
2020-01-14Merge PR #11392: Document the Set Default Proof Mode command.Théo Zimmermann
2020-01-14[coqdoc] Fix #11353: coqdoc -g omits all sentences with decorationsKarl Palmskog
2020-01-14Document the Set Default Proof Mode command.Pierre-Marie Pédrot
2020-01-14Merge PR #10486: [extraction] Support extraction of Coq's string type to OCam...Kazuhiko Sakaguchi
2020-01-13Merge PR #11081: Native compute: cleanup temporary files on program exitPierre-Marie Pédrot
2020-01-13Native compute: cleanup temporary files on program exitGaëtan Gilbert
2020-01-13Merge PR #11285: fix #11279. Specialize h no longer expands letins in the typ...Pierre-Marie Pédrot
2020-01-13Merge PR #11280: Fix #11195 and add other improvements: try loading .vio (and...Pierre-Marie Pédrot
2020-01-12fix #11279. Specialize h no longer expands letins in the type of h.Pierre Courtieu
2020-01-11Merge PR #11367: Minor cleanup of indtypes/indtypingPierre-Marie Pédrot
2020-01-11Merge PR #11349: [refman] [changelog] Announce omega replacement.Pierre-Marie Pédrot
2020-01-10Merge PR #11387: [refman] missing space in "Controlling the locality of comma...Théo Zimmermann
2020-01-10Merge PR #11385: Add badges for Docker Hub and coqorg/coq:latest versionThéo Zimmermann
2020-01-10missing spaceOlivier Laurent
2020-01-10Merge PR #11384: Fix build after merge of #11164Pierre-Marie Pédrot
2020-01-09Merge PR #11371: [merge script] Never bypass outdated branch sanity check.Jason Gross
2020-01-09Add badges for Docker Hub and coqorg/coq:latest versionErik Martin-Dorel
2020-01-09Fix build after merge of #11164Gaëtan Gilbert
2020-01-09Merge PR #11164: [CS] allow Let variable to be canonicalPierre-Marie Pédrot
2020-01-08Merge PR #11375: Add note about default goal selector next to bullet docsThéo Zimmermann
2020-01-08Merge PR #11378: let CI test bedrock2's 'tested' branch instead of 'master'Théo Zimmermann
2020-01-08Add Set NativeCompute TimingJason Gross
2020-01-08let CI test bedrock2's 'tested' branch instead of 'master'Samuel Gruetter
2020-01-08Add note about default goal selector next to bullet docsGaëtan Gilbert
2020-01-08Add changelog entry for native string extractionMaxime Dénès
2020-01-08Add test case for string extraction in OCaml and HaskellMaxime Dénès
2020-01-08Factorize ascii extraction in ExtrOcamlChar.vMaxime Dénès
2020-01-08Better extraction of string literals in HaskellMaxime Dénès
2020-01-08Add documentation for extraction of ascii and string literalsMaxime Dénès
2020-01-08Reimplement string <-> char list conversionsXavier Leroy
2020-01-08Typo in commentXavier Leroy
2020-01-08Rename ExtrOcamlStringPlus into ExtrOcamlNativeStringXavier Leroy
2020-01-08Avoid hardcoded paths in extractionMaxime Dénès
2020-01-08Avoid warning 40Maxime Dénès
2020-01-08Hide ExtrOcamlStringPlus.v like the other extraction filesXavier Leroy
2020-01-08Support extraction of Coq's string type to OCaml's string type, continuedXavier Leroy
2020-01-08Support extraction of Coq's string type to OCaml's string typeXavier Leroy
2020-01-08Close #11133Gaëtan Gilbert
2020-01-08replace deprecated -quick with -vio in the test suiteEnrico Tassi
2020-01-08Close #11168Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 19:21:55 +0000