aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2020-01-08[refman] [changelog] Announce omega replacement.Théo Zimmermann
2020-01-08Merge PR #11341: Add non-utf8 timing testPierre-Marie Pédrot
2020-01-08Update doc/changelog/02-specification-language/11368-trailing_implicit_error.rstSimonBoulier
2020-01-08Trailing implicit: Maxime's suggestionsSimonBoulier
2020-01-07[merge script] Never bypass outdated branch sanity check.Théo Zimmermann
2020-01-07Merge PR #11245: [tools] Remove support for python2Théo Zimmermann
2020-01-07Merge PR #11369: [refman] Correct manual about implicit parameters in inductivesThéo Zimmermann
2020-01-07Merge PR #11317: Fix #11140: Bidirectionality hints perform (surprising?) sim...Enrico Tassi
2020-01-07Correct manual about implicit parameters in inductives.SimonBoulier
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 11:03:18 +0000