aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-01-15generate variance data for section universes (not yet used)Gaëtan Gilbert
preparation for direct discharge
2020-01-14infercumulativity: take less argumentsGaëtan Gilbert
2020-01-14Merge PR #11392: Document the Set Default Proof Mode command.Théo Zimmermann
Reviewed-by: Zimmi48
2020-01-14Document the Set Default Proof Mode command.Pierre-Marie Pédrot
Fixes #10909: Set Default Proof Mode is not documented.
2020-01-14Merge PR #10486: [extraction] Support extraction of Coq's string type to ↵Kazuhiko Sakaguchi
OCaml's string type Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Reviewed-by: herbelin Ack-by: maximedenes Reviewed-by: pi8027
2020-01-13Merge PR #11081: Native compute: cleanup temporary files on program exitPierre-Marie Pédrot
Reviewed-by: JasonGross Reviewed-by: Zimmi48 Reviewed-by: maximedenes Reviewed-by: ppedrot
2020-01-13Native compute: cleanup temporary files on program exitGaëtan Gilbert
We make a temporary directory for these files and cleanup at process exit. The temporary directory means we don't have to guess what extensions ocaml will produce, we can just delete everything there. We use Lazy to avoid spamming unused directories when ahead-of-time compiling without actually using native casts / nativenorm (typically stdlib files). Sadly ocaml has "create temp file" but not "create temp dir", so we have to copy the name generation code. Fix #10495
2020-01-13Merge PR #11285: fix #11279. Specialize h no longer expands letins in the ↵Pierre-Marie Pédrot
type of h. Reviewed-by: ppedrot
2020-01-13Merge PR #11280: Fix #11195 and add other improvements: try loading .vio ↵Pierre-Marie Pédrot
(and not just… Reviewed-by: Zimmi48 Reviewed-by: gares Reviewed-by: ppedrot
2020-01-12fix #11279. Specialize h no longer expands letins in the type of h.Pierre Courtieu
The type of h is reconstructed to look as much as the initial type of h as possible.
2020-01-11Merge PR #11367: Minor cleanup of indtypes/indtypingPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-11Merge PR #11349: [refman] [changelog] Announce omega replacement.Pierre-Marie Pédrot
Ack-by: ejgallego Reviewed-by: maximedenes
2020-01-10Merge PR #11387: [refman] missing space in "Controlling the locality of ↵Théo Zimmermann
commands" Reviewed-by: Zimmi48
2020-01-10Merge PR #11385: Add badges for Docker Hub and coqorg/coq:latest versionThéo Zimmermann
Reviewed-by: Zimmi48
2020-01-10missing spaceOlivier Laurent
2020-01-10Merge PR #11384: Fix build after merge of #11164Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-09Merge PR #11371: [merge script] Never bypass outdated branch sanity check.Jason Gross
Reviewed-by: JasonGross
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
Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Reviewed-by: ppedrot
2020-01-08Merge PR #11375: Add note about default goal selector next to bullet docsThéo Zimmermann
Reviewed-by: Zimmi48
2020-01-08Merge PR #11378: let CI test bedrock2's 'tested' branch instead of 'master'Théo Zimmermann
Reviewed-by: Zimmi48
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
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-08replace deprecated -quick with -vio in the test suiteEnrico Tassi
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-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-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-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>
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 17:31:37 +0000