aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-03-27Fix changelogVincent Semeria
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-27Cleanup stdlib reals. Use implicit arguments for ConstructiveReals. Move ↵Vincent Semeria
ConstructiveReals into new directory Abstract. Remove imports of implementations inside those Abstract files. Add changelog for constructive reals cleanup Move Cauchy reals into new directory Cauchy Update stdlib index Rename sum_f_R0 Use coqdoc comments Update doc/changelog/10-standard-library/11725-cleanup-reals.rst Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com> Update doc/changelog/10-standard-library/11725-cleanup-reals.rst Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com> Update doc/changelog/10-standard-library/11725-cleanup-reals.rst Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com> Improve notations
2020-03-27Helping issue #11659 by leaving only the Cast hack in the grammar.Hugo Herbelin
We clean the hack bypassing the interpretation of "'pat" in binders and move it to comDefinition.ml. In particular, we fix the exact subterm to which Eval has to apply in the hack, and remove the artificial cast we had introduced.
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-26Fix calling test suite makefile with a dune built coqGaëtan Gilbert
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-25[gramlib] Don't expose unsafe interfaces to clientsEmilio Jesus Gallego Arias
I'd say this is more of a temporary measure than a long-term plan; IMO we should make the interfaces safe so `Gramlib.Grammar` does provide only one signature.
2020-03-25[pcoq] Inline the exported Gramlib interface instead of exposing it as GEmilio Jesus Gallego Arias
2020-03-25[parsing] Move comments lexer extensions to base lexer interfaceEmilio Jesus Gallego Arias
This makes sense as a step towards a more functional handling of the state.
2020-03-25[gramlib] Remove warning function parameter in favor of standard mechanism.Emilio Jesus Gallego Arias
If we need more fine-tuning we should manage the warnings with the standard Coq mechanism.
2020-03-25[parsing] Move `coq_parsable` custom logic to Grammar.Emilio Jesus Gallego Arias
Latest refactorings allow us to make the signature Coq parser a standard `Grammar.S` one; the only bit needed is to provide the extra capabilities to the `Lexer` signature w.r.t. to comments state. The handling of Lexer state is still a bit ad-hoc, in particular it is global whereas it should be fully attached to the parsable. This may work ok in batch mode but the current behavior may be buggy in the interactive context. This PR doesn't solve that but it is a step towards a more functional solution.
2020-03-25[parsing] Remove redundant interfaces from PcoqEmilio Jesus Gallego Arias
There is not need to re-export Gramlib's API in a non-structured way anymore. We thus expose the core Gramlib interface to users and remove redundant functions. A question about whether to move more parts of the API to `Gramlib` is still open, as well as on naming.
2020-03-25[parsing] Remove unneeded `Extend.entry` type.Emilio Jesus Gallego Arias
This is not needed anymore after the unification.
2020-03-25[parsing] Remove extend AST in favor of gramlib constructorsEmilio Jesus Gallego Arias
We remove Coq's wrapper over gramlib's grammar constructors.
2020-03-25[parsing] Make grammar rules private.Emilio Jesus Gallego Arias
After the gramlib merge and the type-safe interface added to it, the grammar extension type is redundant; we thus make it private as a first step on consolidating it with the one in gramlib's.
2020-03-25[parsing] Make grammar extension type private.Emilio Jesus Gallego Arias
After the gramlib merge and the type-safe interface added to it, the grammar extension type is redundant; we thus make it private as a first step on consolidating it with the one in gramlib's.
2020-03-25[gitlab] Increase flambda stack size.Emilio Jesus Gallego Arias
See https://github.com/ocaml/ocaml/issues/7842
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-25Make the level of ≡ in Int63 consistent with =Jason Gross
Fixes #11905
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 21:17:01 +0000