aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-03-30[comFixpoint] Minor cleanups in type declarations.Emilio Jesus Gallego Arias
2020-03-30[lemmas] [internal] Reify handling of mutual assumptionsEmilio Jesus Gallego Arias
This gets us closer to the code in `DeclareDef` for the non-interactive case.
2020-03-30[proof] Miscellaneous cleanup on proof info handlingEmilio Jesus Gallego Arias
After the refactorings proof information is organized in a slightly different way thus the lower layers don't need to pass info back anymore.
2020-03-30[lemma] Remove special case for first constant in mutual definition save path.Emilio Jesus Gallego Arias
This could still use some more work due to the way proofs are structured, in particular: - the handling of the primary type w.r.t. Econstr - refining Info.t so open/close invariants hold by typing Very interestingly, better typing means that the tension between tension between `start_dependent_lemma` and the handling of mutual definitions starts to surface. In particular, the information contained in `Info.thms` is not to be used by all non-standard terminators. However, it seems that such refactoring would better fit once we have finished cleaning up the regular save path.
2020-03-31Merge PR #11647: [rfc] Consolidation of parsing interfacesPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-03-30Merge PR #11725: Cleanup stdlib reals.Hugo Herbelin
Ack-by: SkySkimmer Reviewed-by: herbelin
2020-03-30Merge PR #11969: ocamlformat: use whitelist instead of blacklistEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-03-30Merge PR #11965: Partial revert of #11817.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-03-30Merge PR #11968: Fix commit hook when there are no changes (eg amend message)Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-03-30ocamlformat: use whitelist instead of blacklistGaëtan Gilbert
Using disable=true in .ocamlformat and disable=false in sub .ocamlformat works fine. Note that disable=true must be after the `profile` setting otherwise it gets reset
2020-03-30Fix commit hook when there are no changes (eg amend message)Gaëtan Gilbert
Fix #11967
2020-03-30Missing apartness notationsVincent Semeria
2020-03-30Partial revert of #11817.Pierre-Marie Pédrot
The completion proposals need to be ordered by length first for usability. I aknowledge that it's too easy to mess up when refactoring, but here there was a clear comment that this change should not have been performed.
2020-03-30Merge PR #11921: Remove some cruft from Reductionops API.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: gares
2020-03-30Merge PR #11817: [cleanup] Remove unnecessary Map/Set module creationGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: herbelin Ack-by: ppedrot
2020-03-30Merge PR #11951: Remove a useless reversed variant in Vars.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-30Merge PR #11958: Add -no-update command line option to doc_grammar for DuneThéo Zimmermann
Reviewed-by: Zimmi48
2020-03-30Merge PR #11018: “auto with zarith”: use “lia” rather than “omega”Maxime Dénès
Ack-by: Zimmi48 Reviewed-by: anton-trunov Ack-by: jfehrle Reviewed-by: maximedenes
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-29Add -no-update command line option to doc_grammar for DuneJim Fehrle
Fix makefile glitches
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 a useless reversed variant in Vars.Pierre-Marie Pédrot
2020-03-28Remove some cruft from Reductionops API.Pierre-Marie Pédrot
- Removal of exported types and functions that were unused. - Moving ad-hoc functions that were used once in the codebase to their call site.
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-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-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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 14:47:18 +0000