| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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
|
|
That release includes non trivial changes related C compilers, in
particular due to `-fno-common` support.
|
|
Reviewed-by: jfehrle
|
|
Add headers to a few files which were missing them.
|
|
|
|
plugins (e.g. gappa)
Reviewed-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
|
|
Ack-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
|
|
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
and removed the now incorrect "section 8.2.3" reference, as it is the same as the "refine" link.
|
|
Reviewed-by: cpitclaudel
|
|
Reviewed-by: cpitclaudel
|
|
|
|
|
|
|
|
Since version 1.0.0 of the sphinxcontrib-bibtex extension, parallel
building of the Sphinx documentation emits a warning (and thus makes
our warning-free build fail).
This change was already done in Makefile.doc as part of #11732.
|
|
|
|
Same as #11780 except that this part can be backported to v8.11.
|
|
|
|
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: maximedenes
|
|
following the model of `pose (x:=t)`.
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
"where"-based notation
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
Reviewed-by: vbgl
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
|
|
This PR refactors the handling of ML loadpaths to get it closer to
what (as of 2020) the standard OCaml toolchain (ocamlfind, dune) does.
This is motivated as I am leaning toward letting the standard OCaml
machinery handle OCaml includes; this has several benefits [for
example plugins become regular OCaml libs] It will also help in
improving dependency handling in plugin dynload.
The main change is that "recursive" ML loadpaths are no longer
supported, so Coq's `-I` option becomes closer to OCaml's semantics.
We still allow `-Q` to extend the OCaml path recursively, but this may
become deprecated in the future if we decide to install the ML parts
of plugins in the standard OCaml location.
Due to this `Loadpath` still hooks into `Mltop`, but other than that
`.v` location handling is actually very close to become fully
independent of Coq [thus it can be used in other tools such coqdep,
the build system, etc...]
In terms of vernaculars the changes are:
- The `Add Rec ML Path` command has been removed,
- The `Add Loadpath "foo".` has been removed. We now require that the
form with the explicit prefix `Add Loadpath "foo" as Prefix.` is used.
We did modify `fake_ide` as not to add a directory with the empty
`Prefix`, which was not used. This exposed some bugs in the
implementation of the document model, which relied on having an
initial sentence; we have workarounded them just by adding a dummy one
in the two relevant cases.
|
|
- zify_iter_specs is entirely in OCaml
- zify_op has been improved
* The generation of proof-terms is more direct
* It does not `rewrite` but instead either performs
a `pose proof` or a `change`
* The support for `and`, `or`, `not`, arrow is hardcoded
* Avoid generating duplicate hypotheses such as 0 <= Z.of_nat x
- zify_elim_let is entirely in OCaml (no Ltac callback)
[micromega] fix stack overflow
Less naive computation of bounds (online elimination of duplicates)
|
|
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
This is to be consistent with "pose (x:=a)" (and an alternative to
"assert (x:=a)").
This was suggested by
"https://github.com/HoTT/HoTT/pull/1208#discussion_r374342962".
|
|
Reviewed-by: cpitclaudel
|
|
Ack-by: ejgallego
Ack-by: gares
Ack-by: herbelin
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
|
|
|
|
Interestingly, the documentation for Hint Resolve -> qualid was outdated.
It was claiming that any term would be accepted, but actually with this
particular syntax, only qualified names would be parsed already.
|
|
We restrict hints to be global references, so as to further simplify the
implementation. Allowing arbitrary terms makes it difficult or expensive
to handle properly some actions like universe contexts or hint equality.
Ultimately, the IsConstr constructor for hints should also be removed.
|
|
|
|
Reviewed-by: ejgallego
|
|
|
|
|
|
|
