aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2020-01-07Trailing implicit error: documentationSimonBoulier
2020-01-07Trailing implicit error: changelogSimonBoulier
2020-01-07Trailing implicit error: overlaysSimonBoulier
2020-01-07cleanup: do not use recargs when computing the reloc table for ctorsGaëtan Gilbert
2020-01-07minor cleanup template_polymorphic_univs: check_levels returns boolGaëtan Gilbert
2020-01-07Fix test-suite fo non maximal implicit argumentsSimonBoulier
2020-01-07Turn trailing implicit warning into an errorSimonBoulier
2020-01-07[coercions] more precise type for coercion tracesMaxime Dénès
2020-01-06doc: mention limitation of bidi hints vs programGaëtan Gilbert
2020-01-06Fix #11140: Bidirectionality hints perform (surprising?) simplificationMaxime Dénès
2020-01-06[micromega] fix of bug #11191Frédéric Besson
2020-01-06Merge PR #11361: Fix #11360: discharge of template inductive with param only ...Pierre-Marie Pédrot
2020-01-06Merge PR #11340: [refman] Fix bad quoting practice leftover from Sphinx migra...Clément Pit-Claudel
2020-01-06stdlib List: add [remove'] and [count_occ']Yishuai Li
2020-01-06Merge PR #11211: Fixing status reporting for complexity testsGaëtan Gilbert
2020-01-06Fix #11360: discharge of template inductive with param only use of varGaëtan Gilbert
2020-01-05apply suggestions of @anton-trunovOlivier Laurent
2020-01-05clean some indentationsOlivier Laurent
2020-01-04Fixing status reporting for complexity tests.Hugo Herbelin
2020-01-03Merge PR #11343: fix: Shorten ssrsetoid.v to fix TC performance issueEnrico Tassi
2020-01-03Merge PR #11357: coq_makefile: don't use CAMLPKGS when building cmxa of mllibEnrico Tassi
2020-01-03Merge PR #11295: Use code owner teams for every component.Maxime Dénès
2020-01-03coq_makefile: test with CAMLPKGS and mllibGaëtan Gilbert
2020-01-03coq_makefile: don't use CAMLPKGS when building cmxa of mllibGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-11 05:06:20 +0000