| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
One of them revealed a true bug.
|
| |
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
| |
This made little sense, as all the uses of this function were actually
called from toplevel ML modules. This was at best useless, and at worst
a source of bugs when loading plugins and messing with backtracking.
|
| |
|
|
|
| |
Instead of leaving the responsibility of extending the grammar to the caller,
we ask for a list of extensions in the return value of the function.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
This was probably wreaking havoc in tricky undo-redo scenarii.
|
| | |
|
| |
|
|
|
|
|
| |
This removes the last call to unsafe_grammar_extend, so that all handwritten
grammar extensions are now type-safe. Grammars defined by CAMLPX EXTEND are
still using the unsafe interface, but as they insert explicit casts they are
deemed safe.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |\ |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
This reverts commit bde36d4b00185065628324d8ca71994f84eae244.
|
| | |
| |
| |
| | |
This reverts commit 857dc0aaae30805725da213b6550dc1ff3a7adb2.
|
| | | |
|
Hugo Herbelin
Pierre-Marie Pédrot
Maxime Dénès
Guillaume Melquiond
Pierre Letouzey
Daniel de Rauglaudre
Matthieu Sozeau
Emilio Jesus Gallego Arias