| Age | Commit message (Collapse) | Author |
|---|
|
gallina-ext chapter.
|
|
|
|
Reviewed-by: cpitclaudel
|
|
Reviewed-by: Lysxia
Reviewed-by: Zimmi48
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: erikmd
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
|
|
|
|
We propose to add an environment to have foldable texts with HTML
output, more precisely:
(*begin details [: An optional summary] *)
some Coq and documentation material
(* end details *)
Currently, only the HTML output is supported. We could treat this
environment in LaTeX output as appendixes to output later.
|
|
This octopus merge is meant to preserve the commit history / blame of
both parts.
|
|
|
|
(It was moved out onto a separate page.)
|
|
|
|
one. Fix build of PDF manual.
Reviewed-by: cpitclaudel
|
|
|
|
Reviewed-by: Zimmi48
|
|
As CIC is really an acronym, it should be printed in all-caps.
|
|
|
|
|
|
|
|
For instance, parsing 0.1 will print a warning whereas parsing 0.5 won't.
|
|
Remove unneeded source and output files
Move all commands under command NT
Add a lot of edits for commands and tactics
|
|
|
|
coq_config
Reviewed-by: Zimmi48
|
|
|
|
Make sure that all initial load vernaculars that were specified on the command line are executed before processing the options set through -set on the command line.
The reason for this is that the load vernacular options can load plugins that define new Goptions. If these plugins are not loaded before the -set flags are processed,
then Goptions will emit a warning that the options of that plugin don't exist and ignore the flag.
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: jfehrle
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: gares
|
|
Reviewed-by: jfehrle
|
|
fixed bug
Reviewed-by: Zimmi48
|
|
|
|
Unfortunately, we cannot go further and parse Export as a legacy
attribute because this syntax conflicts with the Export command.
|
|
And fix documentation following the removal of the Template Check flag
in #11546.
|
|
|
|
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: jfehrle
|
|
Add headers to a few files which were missing them.
|
|
|
|
Reviewed-by: Zimmi48
|
|
|
|
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: Zimmi48
Reviewed-by: mattam82
Reviewed-by: maximedenes
|
|
following the model of `pose (x:=t)`.
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
|
