| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
| |
immediately in the scope of another recursive pattern.
|
| |
|
| |
|
|
|
|
|
|
|
|
| |
In particular, it becomes possible to have recursive patterns used
shared by binders and terms.
Currently limited by alpha-conversion issues (e.g. test2 from 4932.v
is not reprinted).
|
|
|
|
|
|
|
|
|
|
|
| |
This application was actually not anticipated. It is nice and was not
too difficult to support.
Design for pattern binders maybe to clarify. When seing pat(x1,..,xn)
as a term, I just reused pat(x1,..,xn), but maybe it is worth using
the variable aliasing the pattern, for more a concise notation. But at
the same time, this means exposing the internal name of the alias
which is not so elegant.
|
|
|
|
|
| |
This happens when recursive notations are used to define recursive
notations.
|
| |
|
|\ |
|
| |
| |
| |
| |
| |
| | |
This maintains compatibility, it is debatable if we should use implicit
type information for lets to allow for coercions to fire.
(Problem found in math-comp).
|
| | |
|
|/
|
|
| |
They were allowing algebraic universes to slip in terms.
|
|\ |
|
| |
| |
| |
| |
| |
| | |
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
| |
| |
| |
| | |
See 4865.v for details.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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
|
| | |
|
| |
| |
| |
| | |
They can apply to the head reference under a notation.
|
| |
| |
| |
| |
| |
| | |
internalization.
Patch by PMP, test-suite fix by MS.
|
|\ \
| | |
| | |
| | | |
Was PR#223: Allow feedback messages to carry a location.
|
| | | |
|
| | |
| | |
| | |
| | |
| | | |
(Because the function is private to the module, it is documented in
the .ml rather than the .mli)
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The type of the user-defined function "completer" changes to be
simpler and better reflect its purpose: provide values for missing
field assignments. In the future we may want to also pass the name of
the field as parameter (currently only the index is given, and both
uses of the function ignore it), in particular if we want to implement
{ r with x = ...; y = ... }.
|
| | |
| | |
| | |
| | |
| | | |
The internal `add_pat` function is replaced by a call to
`CList.extract_first`.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The code was a big "try..with" defining all useful quantities at
once. I tried to lift definitions out of this try..with to define them
as early as possible: the record's information and the first field
name are fetched before processing the other fields.
There were two calls in the try..with body that could raise the
Not_found exception (or at least I don't know the code well enough to
be sure that either of them cannot): `shortest_qualid_of_global` and
`build_patt`. They are now split in two separate try..with blocks,
both raising the same exception (with a shared error message named
`env_error_msg`). Someone familiar with the invariants at play could
probably remove one of the two blocks, streamlining the code even
further.
I'm a bit surprised by the main logic part (the big (if .. else if
.. else if ..) block in the new code), and there is a question in
a comment. I hope to get it answered during code review and remove it
(and maybe simplify the code).
Finally, there was an apparently-stale comment in the code:
(* insertion of Constextern.reference_global *)
of course Constextern.reference_global corresponds to now function
that I could find. After trying to understand the meaning of this
comment, I decided to just remove it.
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Note that turning
let boolean = not regular in
if boolean && complete then ...;
if boolean && complete then ...;
into
if not regular && complete then ...;
if not regular && complete then ...;
has absolutely no performance cost: negation inside a conditional is
not computed as a boolean, it only flips the branches. The code is
more readable because "boolean" was a terrible variable name.
|
| | |
| | |
| | |
| | | |
Cf CHANGES for details.
|
|/ /
| |
| |
| |
| |
| |
| |
| | |
This is a first step to relay location info in an uniform way, as needed
by warnings and other mechanisms.
The location info remains unused for now, but coqtop printing could take
advantage of it if so wished.
|
| | |
|
| |
| |
| |
| |
| | |
simplifying and generalizing the grammar entries for injection,
discriminate and simplify_eq.
|
| |
| |
| |
| | |
implicit arguments when in beautification mode.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
computing the arguments which allows to decide which list of implicit
arguments to consider when several such lists are available.
For instance, "eq_refl (A:=nat)" is now interpreted as "@eq_refl nat _",
the same way as if we had said:
Arguments eq_refl {A} {x}.
|
|\ \ |
|
|\ \ \
| | |/
| |/| |
|
| | |
| | |
| | |
| | |
| | | |
We delay the externalization of application arguments in Constrextern,
so that they only get computed when they are actually explicitly displayed.
|
| |/
|/| |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
functions about interpretation, internalization, externalization of
notations.
Main syntactic changes:
- subst_aconstr_in_glob_constr -> instantiate_notation_constr
(because aconstr has been renamed to notation_constr long time ago)
- extern_symbol -> extern_notation
(because symbol.ml has been renamed to notation.ml long time ago)
- documentation of notations_ops.mli
Main semantic changes:
- Notation_ops.eq_glob_constr which was partial eq disappears: use
glob_constr_eq instead
- In particular, this impacts a change on funind which now use the
(fully implemented) glob_constr_eq
Somehow, instantiate_notation_constr should be in notation_ops.ml for
symmetry with match_notation_constr but it is bit painful to do.
|
| |
| |
| |
| | |
and Evar in notations, and there are anyway already forbidden.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
|
| | |
|
| | |
|
| | |
|
|\| |
|
| |
| |
| |
| | |
A single terminal character can take up to 5 bytes, e.g. "''^A'".
|
| |
| |
| |
| | |
rejected.
|
| |
| |
| |
| | |
This reverts commit dbe29599c2e9bf49368c7a92fe00259aa9cbbe15.
|
| |
| |
| |
| | |
This reverts commit f7ea0193c1aac918d8ed2df0d53df38dde5d1152.
|
| |
| |
| |
| | |
This reverts commit 2211eeda012477b26081738fccc59aa31fb0a565.
|