aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-03-30Merge PR #11874: Auto-format micromega files in pre-commit hook.Emilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego
2020-03-29Merge PR #11938: Support for updating orderedGrammar with Dune.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-03-29Merge PR #11859: Warn when non exactly parsing non floating-pointHugo Herbelin
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: erikmd
2020-03-29Merge PR #11944: Remove SearchAbout command, deprecated in 8.5Théo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-03-28Merge PR #11950: Document change of behavior of Fail in 8.11.Clément Pit-Claudel
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
2020-03-28Document change of behavior of Fail in 8.11.Théo Zimmermann
2020-03-28Update fullGrammar and orderedGrammar following #11877.Théo Zimmermann
2020-03-28New target check-gram to check if fullGrammar and orderedGrammar are up-to-date.Théo Zimmermann
Use `dune build @check-gram --auto-promote` to automatically update these two files. You will need to run it twice if the two files need to be updated (which is the case most often) as Dune will stop after the first diff failure. The rst files are also updated but left in the `_build/` directory as Dune wouldn't support targets outside the current directory. You can just `mv _build/default/doc/sphinx doc` to update them after running the @check-gram target.
2020-03-27Merge PR #11809: [configure] Remove `-std=c99` from default C flagsJason Gross
Reviewed-by: JasonGross Ack-by: SkySkimmer
2020-03-27Merge PR #11871: Split documentation of coqdoc on separate page.Clément Pit-Claudel
2020-03-27[configure] Remove `-std=c99` from default C flagsEmilio Jesus Gallego Arias
Recent OCaml don't allow to build the VM with `--std=c99` anymore due to changes in header files. `gnu99` is required, but it turns out this is already enforced by OCaml, so we just remove the flag altogether. See the discussion in #11432
2020-03-27Merge PR #11848: Nicer printing for decimal constantsHugo Herbelin
Reviewed-by: herbelin
2020-03-27Merge PR #11751: Fix #11749: don't warn for hidden files.Maxime Dénès
Reviewed-by: maximedenes
2020-03-27Merge PR #11102: Use the Alloc_small macro from the OCaml runtime rather ↵Maxime Dénès
than our own. Ack-by: aaronpuchert Ack-by: gadmm Reviewed-by: maximedenes Ack-by: ppedrot Reviewed-by: proux01
2020-03-27Split coqdoc section out of utility chapter (octopus merge).Théo Zimmermann
This octopus merge is meant to preserve the commit history / blame of both parts.
2020-03-27Move section on coqdoc to new location.Théo Zimmermann
2020-03-27Remove the part about coqdoc from the utilities chapter.Théo Zimmermann
(It was moved out onto a separate page.)
2020-03-27Prepare split of section about coqdoc.Théo Zimmermann
2020-03-27Merge PR #11925: [ci] Add bbvEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-03-26Merge PR #11929: Reintroduce a command that was actually used in another ↵Clément Pit-Claudel
one. Fix build of PDF manual. Reviewed-by: cpitclaudel
2020-03-26Reintroduce commands that were actually used. Fix build of PDF manual.Théo Zimmermann
2020-03-26Merge PR #11877: Removing deprecated destruct/remember syntax _eqn.Théo Zimmermann
Reviewed-by: Zimmi48
2020-03-26Change logHugo Herbelin
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
2020-03-26Merge PR #11920: Shrink refman-prelude files.Clément Pit-Claudel
Ack-by: SkySkimmer Reviewed-by: cpitclaudel
2020-03-26[ci] Add bbvJason Gross
I believe a recent commit to master broke it, and now that it's no longer tested as part of fiat-crypto-legacy, I think it's time to add it.
2020-03-26CIC is printed in all-caps.Théo Zimmermann
As CIC is really an acronym, it should be printed in all-caps.
2020-03-26Removing deprecated destruct syntax _eqn.Hugo Herbelin
2020-03-26Shrink refman-prelude files.Théo Zimmermann
2020-03-26Merge PR #11918: Fix #11845: anomaly when including partially applied functorPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-26Merge PR #11919: Remove outdated mention of -allow-sprop.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-26Remove outdated mention of -allow-sprop.Théo Zimmermann
2020-03-26Fix #11845: anomaly when including partially applied functorGaëtan Gilbert
2020-03-26Merge PR #11913: Doc_grammar: Update cmd:: and tacn:: constructs in .rstsThéo Zimmermann
Reviewed-by: Zimmi48
2020-03-26Merge PR #11832: [ocamlformat] Use doc-comments=before style.Théo Zimmermann
Reviewed-by: Zimmi48
2020-03-26Merge PR #11885: Sorting: Swap the names of Sorted_sort and LocallySorted_sortHugo Herbelin
Reviewed-by: herbelin
2020-03-26Merge PR #11891: Fix levels of `<=?` and `<?` in the stdlibHugo Herbelin
Reviewed-by: herbelin
2020-03-26Print a warning when parsing non floating-point values.Pierre Roux
For instance, parsing 0.1 will print a warning whereas parsing 0.5 won't.
2020-03-25Merge PR #11898: Switch opam file to makeEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-03-25[ocamlformat] Use doc-comments=before style.Emilio Jesus Gallego Arias
IMHO it is a bit more logical, WDYT?
2020-03-25Doc_grammar: Update cmd:: and tacn:: constructs in .rstsJim Fehrle
Remove unneeded source and output files Move all commands under command NT Add a lot of edits for commands and tactics
2020-03-25Merge PR #11705: Convert Gallina Extensions chapter to use prodnsThéo Zimmermann
Ack-by: Zimmi48
2020-03-25Convert Gallina Extensions to use prodnJim Fehrle
2020-03-25Merge PR #11785: [proof] consolidation of mutual definition declaration pathGaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: herbelin Reviewed-by: ppedrot
2020-03-25Merge PR #11875: Fix deploy of refman following #11855.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: ejgallego
2020-03-25Update changelogPierre Roux
2020-03-25Nicer printing for decimal constants in QPierre Roux
Print 1.5 as 1.5 and not 15e-1. We choose the shortest representation with tie break to the dot notation (0.01 rather than 1e-3). The printing remains injective, i.e. 12/10 is not mixed with 120/100, the first being printed as 1.2 and the last as 1.20.
2020-03-25Nicer printing for decimal constants in RPierre Roux
Print 1.5 as 1.5 and not 15e-1. We choose the shortest representation with tie break to the dot notation (0.01 rather than 1e-3). The printing remains injective, i.e. 12*10^2 is printed 12e2 in order not to mix it with 1200 and 12/10^1 is not mixed with 120/10^2, the first being printed as 1.2 and the last as 1.20.
2020-03-25Add a specific opam file to build te docker imagePierre Roux
The Docker image coqorg/coq:dev is currently built using the OPAM file coq.opam. Since this file is used for develoment purpose, it would be better to use a more stable one for building the docker images. The OPAM option "--locked=docker" will then be used in the opam pin command when building the docker image to use the new coq.opam.docker file. The new file builds Coq using make, this is temporary and could be reverted to dune once it supports "-native-compiler yes".
2020-03-25[declare] make restrict_ucontext an optional parameter.Emilio Jesus Gallego Arias
The current API does just exist as a workaround for a bug.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 19:40:27 +0000