| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: jfehrle
|
|
fixed bug
Reviewed-by: Zimmi48
|
|
Reviewed-by: ppedrot
|
|
|
|
|
|
Reviewed-by: JasonGross
Reviewed-by: Zimmi48
|
|
|
|
As a first step toward a deeper refactoring of the reference manual,
we move existing chapters into a new structure.
We use the Sphinx support for top-level chapters spanning multiple
pages to consolidate existing chapters into a smaller number of
chapters and a smaller number of parts.
Now the full top-level table of content can be seen in one glance.
Most of the new chapters are divided into several sub-chapters (on
separate pages) that correspond to the pre-existing chapters. These
new top-level chapters gathering several chapters together have gained
a new introduction. The main introduction has been rewritten /
simplified as well.
For now, the URL of pre-existing chapters does not change. The intent
is to further refactor the manual by splitting some of these
sub-chapters into smaller ones, and by moving things around.
While the sub-chapters are likely to evolve very much in the future,
the top-level table of content is almost final (except that the "Using
Coq" part may gain one or two additional chapters on proof engineering
/ project management).
Thanks to Jim Fehrle for investigating how to split a chapter on
multiple pages and to both Jim and Matthieu Sozeau for the discussion
that led to this new structure.
See also the related CEP: https://github.com/coq/ceps/pull/43
Additional notes:
- A new directory structure has been created reflecting the new
chapter structure.
- The indexes chapter has been removed from the PDF version since it
wasn't working.
Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
|
|
Reviewed-by: SkySkimmer
|
|
Ack-by: herbelin
|
|
Reviewed-by: JasonGross
Reviewed-by: ppedrot
|
|
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
|
|
|
|
That release includes non trivial changes related C compilers, in
particular due to `-fno-common` support.
|
|
Reviewed-by: JasonGross
Ack-by: SkySkimmer
|
|
|
|
That is, it contains the type of the binder so as not to rely on the relevance
explicitly.
|
|
For robustness and it is better to leave it opaque. Users are not supposed to
fiddle with it.
|
|
Reviewed-by: jfehrle
|
|
Reviewed-by: Zimmi48
Ack-by: gares
Ack-by: maximedenes
|
|
Reviewed-by: ppedrot
|
|
Add headers to a few files which were missing them.
|
|
|
|
|
|
|
|
|
|
Cf. discussion at #11559 and decision of Coq Call 2020-02-26.
|
|
We reuse the same type as for options, even though it is a bit ill-named. At
least it allows to share code with it.
|
|
The current implementation was seemingly never thought for this kind of
semantics. Everything is superglobal by construction, notably hint database
creation and naming schemes. The new mode feels a bit hackish to me, at
some point this should be fully reimplemented from scratch with a clear
design in mind.
|
|
|
|
plugins (e.g. gappa)
Reviewed-by: Zimmi48
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
|
|
We bump ounit, odoc, and lablgtk3 ; so far this is routine maintenance.
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
|
|
VST has been fixed upstream, c.f.
https://github.com/PrincetonUniversity/VST/issues/392
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
|
|
Ack-by: ejgallego
|
|
is contiguous to the number.
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
A constraint can be stuck if it does not match any of the declared modes
for its head (if there are any). In that case, the subgoal is postponed
and the next ones are tried. We do a fixed point computation until there
are no stuck subgoals or the set does not change (it is impossible to
make it grow, as asserted in the code, because it is always a subset of
the initial goals)
This allows constraints on classes with modes to be treated as if they were
in any order (yay for stability of solutions!). Also, ultimately it should
free us to launch resolutions more agressively (avoiding issues like the
ones seen in PR #10762).
Add more examples of the semantics of TC resolution with apply in test-suite
Properly catch ModeMatchFailure on calls to map_e*
Add fixed bug 9058 to the test-suite
Close #9058
Add documentation
Fixes after Gaëtan's review.
Main change is to not use exceptions for control-flow
Update tactics/class_tactics.ml
Clearer and more efficient mode mismatch dispatch
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Remove exninfo argument
|
|
10.13 is deprecated as an azure VM
Close #11449
|
|
>= 4.08 (#11624)
Reviewed-by: ppedrot
|
