| Age | Commit message (Collapse) | Author |
|---|
|
In previous versions of Coq `abstract` could create non-uniform bodies
for mutually recursive definitions (c.f. bug #5065)
Thanks to changes to the trusted base this is not the case anymore,
thus we can remove the workaround.
This way mutual bodies are handled the same in the interactive and
non-interactive case.
|
|
|
|
This gets us closer to the code in `DeclareDef` for the
non-interactive case.
|
|
After the refactorings proof information is organized in a slightly
different way thus the lower layers don't need to pass info back
anymore.
|
|
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.
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: herbelin
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
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
|
|
Fix #11967
|
|
|
|
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.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
Ack-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: Zimmi48
|
|
Ack-by: Zimmi48
Reviewed-by: anton-trunov
Ack-by: jfehrle
Reviewed-by: maximedenes
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
|
|
Fix makefile glitches
|
|
Reviewed-by: ejgallego
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: erikmd
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
|
|
|
|
- Removal of exported types and functions that were unused.
- Moving ad-hoc functions that were used once in the codebase to their call site.
|
|
|
|
|
|
|
|
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.
|
|
|
|
Reviewed-by: JasonGross
Ack-by: SkySkimmer
|
|
|
|
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
|
|
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
|
|
Reviewed-by: herbelin
|
|
Reviewed-by: maximedenes
|
|
than our own.
Ack-by: aaronpuchert
Ack-by: gadmm
Reviewed-by: maximedenes
Ack-by: ppedrot
Reviewed-by: proux01
|
|
This octopus merge is meant to preserve the commit history / blame of
both parts.
|
|
|
|
(It was moved out onto a separate page.)
|
|
|
|
Reviewed-by: ejgallego
|
|
one. Fix build of PDF manual.
Reviewed-by: cpitclaudel
|
|
|
|
Reviewed-by: Zimmi48
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
Ack-by: SkySkimmer
Reviewed-by: cpitclaudel
|
|
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.
|
