| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |\
| |
| |
| | |
record fields.
|
| | |
| |
| |
| |
| |
| |
| |
| | |
We remove the camlp4 compatibility layer, and try to clean up
most structures. `parsing/compat` is gone.
We added some documentation to the lexer/parser interfaces that are
often obscured by module includes.
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This is the good parts of PR #360.
IIUC, these vernacular were meant mostly for debugging and they are
not supposed to be of any use these days.
Back and join are still there not to break the testing infrastructure,
but some day they should go away.
|
| | | |
| | |
| | |
| | | |
RawLocal -> CLocal
|
| |/ / |
|
| |/
|
|
|
|
|
|
|
|
|
|
| |
Note: This reveals a little bug yet to fix in g_vernac.ml4. In
Definition f '((x,y):id nat * id nat) '((x',y'):id nat * id nat) := Eval unfold id in x+y = x'+y'.
the "id" are wrongly unfolded and in
Definition f '(x,y) '(x',y') := x+y = x'+y' : Prop.
an unexpected cast remains in the body of f.
|
| |\ |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| | |
We introduce a bit of compatibility parsing code to print deprecation
warnings.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
This reverts commit b00e039b957b8428c21faec5c76f3a3484cde2cf, reversing
changes made to ca9e00ff9b2a8ee17430398a5e0bef2345c39341.
It turns out that calling from fake_ide the STM commands that were removed
by this PR requires an extension of the XML protocol. So postponing the
integration.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
I think these commands never make a lot of sense on scripts other than
debugging and we have better methods now.
The last remaining command, used for the tty emulation has been renamed
to VtBack, but it should go away at some point too once the legacy
interfaces are removed.
|
| | |\
| | |
| | |
| | | |
Was PR#339: Documenting type class options, typeclasses eauto
|
| | |\ \
| | | |
| | | |
| | | | |
Was PR#340: Fix various shortcomings of the warnings infrastructure.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
In addition to a priority, cleanup the interfaces for passing this
information as well. The pattern, if given, takes priority over the
inferred one.
We only allow Existing Instances gr ... gr | pri. for now, without
pattern, as before.
Make the API compatible to 8.5 as well.
|
| | | |/
| |/|
| | |
| | |
| | | |
With multiple arguments list, repeating the "/" modifier used to be
mandatory. So instead of forbidding it, we issue a deprecation warning.
|
| | |/
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- The flags are now interpreted from left to right, without any other
precedence rule. The previous one did not make much sense in interactive
mode.
- Set Warnings and Set Warnings Append are now synonyms, and have the
"append" semantics, which is the most natural one for warnings.
- Warnings on unknown warnings are now printed only once (previously the
would be repeated on further calls to Set Warnings, sections closing,
module requiring...).
- Warning status strings are normalized, so that e.g. "+foo,-foo" is reduced
to "-foo" (if foo exists, "" otherwise).
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The main point of this change is to fix #3035: Avoiding trailing
arguments in the Arguments command, and related issues occurring in
HoTT for instance. When the "assert" flag is not specified, we now
accept prefixes of the list of arguments.
The semantics of _ w.r.t. to renaming has changed. Previously, it meant
"restore the original name inferred from the type". Now it means "don't
change the current name".
The syntax of arguments is now restricted. Modifiers like /, ! and
scopes are allowed only in the first arguments list.
We also add *a lot* of missing checks on input values and fix various
bugs.
Note that this code is still way too complex for what it does, due to
the complexity of the implicit arguments, reduction behaviors and renaming
APIs.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| | |
This was introduced to implement the Append feature on options. As usual when
messing with predefined keywords, this broke code in the wild. In order not
to create a new keyword, we do the string analysis on the production branch of
parsing.
|
| |\| |
|
| | |
| |
| |
| | |
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.
|
| | |/ |
|
| | | |
|
| |/
|
|
| |
Suggested by @ppedrot
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |\ |
|
| | | |
|
| | | |
|
| |\ \
| | |
| | |
| | | |
into JasonGross-trunk-function_scope
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
Gaetan Gilbert
Maxime Dénès
Emilio Jesus Gallego Arias
Hugo Herbelin
Pierre-Marie Pédrot
Ralf Jung
Matthieu Sozeau
Guillaume Melquiond
Enrico Tassi
Pierre Letouzey
Daniel de Rauglaudre