aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-01-08Add note about default goal selector next to bullet docsGaëtan Gilbert
Close #11036
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
Using only OCaml stdlib functions available in OCaml 4.05.
2020-01-08Typo in commentXavier Leroy
2020-01-08Rename ExtrOcamlStringPlus into ExtrOcamlNativeStringXavier Leroy
As suggested during review. That's a much better name.
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
Address issues found in CI testing and in code review.
2020-01-08Support extraction of Coq's string type to OCaml's string typeXavier Leroy
Instead of the default extraction to OCaml's "char list" type.
2020-01-08Close #11133Gaëtan Gilbert
Fixed by 8750682e367d7e78634bf88e667e4c9e7c3613d3 (#9915)
2020-01-08replace deprecated -quick with -vio in the test suiteEnrico Tassi
2020-01-08Close #11168Gaëtan Gilbert
Seems to have been fixed since it was reported (perhaps by #11317?)
2020-01-08[refman] [changelog] Announce omega replacement.Théo Zimmermann
2020-01-08Merge PR #11341: Add non-utf8 timing testPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-08Update doc/changelog/02-specification-language/11368-trailing_implicit_error.rstSimonBoulier
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
2020-01-08Trailing implicit: Maxime's suggestionsSimonBoulier
2020-01-07[merge script] Never bypass outdated branch sanity check.Théo Zimmermann
The message was confusing and the prompt let one reviewer think the merge script would take care of doing the pull, which it doesn't.
2020-01-07Merge PR #11245: [tools] Remove support for python2Théo Zimmermann
Reviewed-by: JasonGross Reviewed-by: Zimmi48 Reviewed-by: vbgl
2020-01-07Merge PR #11369: [refman] Correct manual about implicit parameters in inductivesThéo Zimmermann
Reviewed-by: Zimmi48
2020-01-07Merge PR #11317: Fix #11140: Bidirectionality hints perform (surprising?) ↵Enrico Tassi
simplification Reviewed-by: SkySkimmer Ack-by: gares Reviewed-by: mattam82
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
This doesn't actually have anything to do with positivity AFAICT, we just want the number of non-parameter arguments.
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
No example as I'm not familiar enough with Program to make one.
2020-01-06Fix #11140: Bidirectionality hints perform (surprising?) simplificationMaxime Dénès
We typecheck arguments like previously, using bidirectionality hints, but ultimately replace them with user-provided arguments on which we replay coercion traces. This is a fix which should be easy to backport, but there are two directions of future work: - Coercion traces for `Program` coercions (in these cases, we currently use the inferred arguments) - Separate the Coercion API in two phases: inference and application of coercions. It will make the approach taken here cleaner, and probably make it easier to interleave typing steps with coercion inference. Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-01-06[micromega] fix of bug #11191Frédéric Besson
- Add an instance to ZifyInst to instruct zify that 0 < x -> 0 < y -> 0 < Z.pow x y - More aggressive interval analysis to bound non-linear monomials.
2020-01-06Merge PR #11361: Fix #11360: discharge of template inductive with param only ↵Pierre-Marie Pédrot
use of var Reviewed-by: mattam82 Reviewed-by: ppedrot
2020-01-06Merge PR #11340: [refman] Fix bad quoting practice leftover from Sphinx ↵Clément Pit-Claudel
migration. Reviewed-by: jfehrle
2020-01-06stdlib List: add [remove'] and [count_occ']Yishuai Li
2020-01-06Merge PR #11211: Fixing status reporting for complexity testsGaëtan Gilbert
Reviewed-by: SkySkimmer
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
The regexp parsing the time needed an update to support the case "Finished failing translation". Also, not all cases of failures were reported.
2020-01-03Merge PR #11343: fix: Shorten ssrsetoid.v to fix TC performance issueEnrico Tassi
Reviewed-by: gares
2020-01-03Merge PR #11357: coq_makefile: don't use CAMLPKGS when building cmxa of mllibEnrico Tassi
Reviewed-by: gares
2020-01-03Merge PR #11295: Use code owner teams for every component.Maxime Dénès
Reviewed-by: maximedenes
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
It seems broken according to unicoq experiences https://gitter.im/coq/coq?at=5e0e3e0005298604982ac3f7 Building cmxa of mlpack is already this way.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 06:32:30 +0000