| Commit message (Collapse) | Author | Age |
|---|
| |\
| |
| |
| | |
Was PR#232: Fix the parsing of goal selectors.
|
| | |
| |
| |
| |
| |
| | |
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
| |/
|
|
|
| |
This fixes some parsing problems when doing things like
[let n := 2 in idtac n]. See bug #4877.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
On the user side, coqtop and coqc take a list of warning names or categories
after -w. No prefix means activate the warning, a "-" prefix means deactivate
it, and "+" means turn the warning into an error. Special categories include
"all", and "default" which contains the warnings enabled by default.
We also provide a vernacular Set Warnings which takes the same flags as argument.
Note that coqc now prints warnings.
The name and category of a warning are printed with the warning itself.
On the developer side, Feedback.msg_warning is still accessible, but the
recommended way to print a warning is in two steps:
1) create it by:
let warn_my_warning =
CWarnings.create ~name:"my-warning" ~category:"my-category"
(fun args -> Pp.strbrk ...)
2) print it by:
warn_my_warning args
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
This commit documents par:, fixes its semantics so that is
behaves like all:, supports (toplevel) abstract and optimizes
toplevel solve.
`par: solve [tac]` is equivalent to `Ltac tac1 := solve[tac]...par: tac1`
but is optimized for failures: if one goal fails all are aborted
immediately.
`par: abstract tac` runs abstract on the generated proof terms. Nested
abstract calls are not supported.
|
| | |
|
| |
|
|
| |
presence of entries starting with a non-terminal such as "b ^2".
|
| |\ |
|
| | |
| |
| |
| | |
They can still be used at the toplevel.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This allows to write things like this:
split; 2: intro _; exact I
or like this:
eexists ?[x]; ?[x]: exact 0; trivial
This has the side-effect on making the '?' before '[x]' mandatory.
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| | |
You can now write [[1, 3-5]:tac.] to apply [tac] on the subgoals
numbered 1 and 3 to 5.
|
| | |
| |
| |
| |
| | |
"par: tac" is a terminator, if it fails we can admit all focused goals
and continue.
|
| |/
|
|
|
|
|
|
|
|
|
|
| |
This commit introduces the concept of proof blocks that are
resilient to errors. They are represented as ErrorBound boxes
in the STM document with the topological invariant that they never
overlap.
The detection and error recovery of ErrorBound boxes is defined outside
the STM. One can define a box by providing a function to detect it
statically by crawling the parsed document and a function to recover
from an error at run time.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This patch splits pretty printing representation from IO operations.
- `Pp` is kept in charge of the abstract pretty printing representation.
- The `Feedback` module provides interface for doing printing IO.
The patch continues work initiated for 8.5 and has the following effects:
- The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`,
`pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`,
`msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be
used instead.
- Feedback provides different backends to handle output, currently,
`stdout`, `emacs` and CoqIDE backends are provided.
- Clients cannot specify flush policy anymore, thus `pp_flush` et al are
gone.
- `Feedback.feedback` takes an `edit_or_state_id` instead of the old
mix.
Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
|
| | |
|
| | |
|
| |
|
|
| |
This reverts commit e01dabf9f7aa530c4c70aadf464097cd102b1df6.
|
| |
|
|
| |
This reverts commit 239f30c2070018db88e568acca6c9054f650ca38.
|
| | |
|
| |
|
|
| |
presence of entries starting with a non-terminal such as "b ^2".
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
pr_vernac.
|
| |
|
Maxime Dénès
Pierre Letouzey
Cyprien Mangin
Enrico Tassi
Hugo Herbelin
Pierre-Marie Pédrot
Emilio Jesus Gallego Arias