| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | |
| |
| |
| | |
This reverts commit 466b7e69e49a5f4bba36b834a2e046f120ece07c.
|
| | |\
| | |
| | |
| | |
| | | |
Was PR#305: A possible solution to the issue of fine-tuning warnings in
script.
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
That way, bullet detection no longer depends on a global variable
indicating whether a line is starting. This causes a small change in the
recognized language. Before the commit, "--++" was recognized as a bullet
"--" followed by a keyword "++" when at the start of a line; now it is
always recognized as a keyword "--++".
This also fixes a bug in Tok.to_string as a side-effect.
|
| | |/
| |
| |
| |
| |
| |
| |
| |
| |
| | |
For now, the only meaningful user is "Set Warnings". Example:
Section Bar.
Local Set Warnings Append "-foo".
(* warning foo is now disabled *)
End Bar.
(* foo is now reenabled, assuming it was before entering the section *)
|
| | |\
| | |
| | |
| | |
| | | |
Was PR#299: Fix bug #4869, allow Prop, Set, and level names in
constraints.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
This is a quick fix. The Metasyntax module should be thoroughly revised
in trunk, because it starts featuring a lot of spaghetti code and redundant
data.
|
| | | |
| | |
| | |
| | |
| | | |
It seems warnings are not taken into account in output/
tests.
|
| | |/ |
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
There was no reason to keep them separate since quite a long time. Historically,
they were making Genarg depend or not on upper strata of the code, but since
it was moved to lib/ this is not justified anymore.
|
| | |
| |
| |
| | |
One of them revealed a true bug.
|
| |\ \
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We untangle many dependencies on Ltac datastructures and modules from the
lower strata, resulting in a self-contained ltac/ folder. While not a plugin
yet, the change is now very easy to perform. The main API changes have been
documented in the dev/doc/changes file.
The patches are quite rough, and it may be the case that some parts of the
code can migrate back from ltac/ to a core folder. This should be decided on
a case-by-case basis, according to a more long-term consideration of what is
exactly Ltac-dependent and whatnot.
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| |/ / |
|
| |\ \
| |/
|/| |
|
| | |
| |
| |
| |
| |
| | |
They were mostly useless, and people complained about it. Not that because
there is no API to make CAMLP4 silent, a CAMLP4-based Coq will still spit
out its share of noisy warnings.
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
Suggested by @ppedrot
|
| | |
| |
| |
| |
| |
| |
| | |
As noted by @ppedrot, the first is redundant. The patch is basically a renaming.
We didn't make the component optional yet, but this could happen in a
future patch.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
| |
In some cases prior to this patch, there were two cases for the same
error function, one taking a location, the other not.
We unify them by using an option parameter, in the line with recent
changes in warnings and feedback.
This implies a bit of clean up in some places, but more importantly, is
the preparation for subsequent patches making `Loc.location` opaque,
change that could be use to improve modularity and allow a more
functional implementation strategy --- for example --- of the
beautifier.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
Apparently, in camlp4 (unlike camlp5) :
- Something like "[ kwd = IDENT "foobar" -> .... kwd ... ]"
produces a kwd of type token instead of string (which sounds reasonable ?).
For now, I've replaced kwd by the explicit strings. Not so nice, but works
with both camlp4 and camlp5
- A quotation of the form "let obj = ... in bar; baz" is not
interpreted in the usual OCaml way, but rather as
"(let obj = ... in bar); baz".
Let's use instead "let obj = ... in let () = bar in baz", which works fine.
|
| | |
|
| |
|
|
|
| |
This was implemented in anticipation of a part of PR#164 that we decided not to
merge.
|
| |
|
|
|
|
| |
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
| |
Cf CHANGES for details.
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Coq locations already had support for this, but were containing dummy
information. We now don't need anymore to reconstruct this information by
browsing the file when printing an error message or enriching exceptions on the
fly.
It also became easier to interface with Coq since locations emitted by the
lexer now always contain full information.
On the API side, Loc.represent disappeared and Loc.t is now exposed as record.
It is less error-prone than manipulating a tuple of 5 integers. Also,
Loc.create takes 5 arguments instead of 3 and a pair.
|
| | |
| |
| |
| |
| | |
simplifying and generalizing the grammar entries for injection,
discriminate and simplify_eq.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
In pat%constr, creating new evars is now allowed only if "eintros" is
given, i.e. "intros" checks that no evars are created, and similarly
e.g. for "injection ... as ... pat%constr".
The form "eintros [...]" or "eintros ->" with the case analysis or
rewrite creating evars is now also supported.
This is not a commitment to say that it is good to have an e- modifier
to tactics. It is just to be consistent with the existing convention.
It seems to me that the "no e-" variants are good for beginners. However,
expert might prefer to use the e-variants by default. Opinions from
teachers and users would be useful.
To be possibly done: do that [= ...] work on hypotheses with side
conditions or parameters based on the idea that they apply the full
injection and not only the restriction of it to goals which are
exactly an equality, as it is today.
|
| |/
|
|
|
| |
It is already very old (shipped with Debian oldstable) and adds file name
support in locations.
|
| |
|
|
|
|
|
| |
Suggested by R. Krebbers and C. Cohen, this makes modes
more applicable, by allowing to trigger resolution on partially
instantiated indices. This is a rough but fast approximation of the
pattern on which one would like instances to apply.
|
| | |
|
| |
|
|
|
|
| |
simpler re-printing of assert.
Also fixing the precedence for printing "by" clause.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
Note that this breaks the compatibility, in a beneficial way I believe. Tactics
defined in strict mode (i.e. through Ltac foo := ...) may not do an introduction
on a local identifier anymore. They must use the "fresh" primitive instead.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
Guillaume Melquiond
Maxime Dénès
Pierre-Marie Pédrot
Enrico Tassi
Matthieu Sozeau
Hugo Herbelin
Emilio Jesus Gallego Arias
Pierre Letouzey
Daniel de Rauglaudre