| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Virtually all classifications of vernacular commands (the STM
classifier, "filtered commands", "navigation commands", etc.) were
broken in presence of control vernaculars like Time, Timeout, Fail.
Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac
Debug in CoqIDE.
This change introduces a type separation between vernacular controls and
vernacular commands, together with an "under_control" combinator.
|
|
We remove deprecated syntax "Coercion Local" and such, and seize the
opportunity to refactor some code around vernac_expr.
We also do a small fix on the STM classification, which didn't know about
Let Fixpoint and Let CoFixpoint.
This is a preliminary step for the work on attributes.
|
|
|
|
When we used to parse to a glob_sort but always give an empty list in
the GType case we can now parse directly to Sorts.family.
|
|
This ensures that the API is self-contained and is, well, an API.
Before this patch, the contents of `API.mli` bore little relation with
what was used by the plugins [example: `Metasyntax` in tacentries.ml].
Many missing types had to be added.
A sanity check of the `API.mli` file can be done with:
`ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli`
|
|
|
|
|
|
|
|
|
|
Reminder of (some of) the reasons for removal:
- Despite the claim in sigma.mli, it does *not* prevent evar
leaks, something like:
fun env evd ->
let (evd',ev) = new_evar env evd in
(evd,ev)
will typecheck even with Sigma-like type annotations (with a proof of
reflexivity)
- The API stayed embryonic. Even typing functions were not ported to
Sigma.
- Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly
less unsafe ones (e.g. s_enter), but those ones were not marked unsafe
at all (despite still being so).
- There was no good story for higher order functions manipulating evar
maps. Without higher order, one can most of the time get away with
reusing the same name for the updated evar map.
- Most of the code doing complex things with evar maps was using unsafe
casts to sigma. This code should be fixed, but this is an orthogonal
issue.
Of course, this was showing a nice and elegant use of GADTs, but the
cost/benefit ratio in practice did not seem good.
|
|
It seems there were 4 copies of the same function in the code base.
|
|
This is the continuation of #244, we now deprecate `CErrors.error`,
the single entry point in Coq is `user_err`.
The rationale is to allow for easier grepping, and to ease a future
cleanup of error messages. In particular, we would like to
systematically classify all error messages raised by Coq and be sure
they are properly documented.
We restore the two functions removed in #244 to improve compatibility,
but mark them deprecated.
|
|
|
|
|
|
This completes the Loc.ghost removal, the idea is to gear the API
towards optional, but uniform, location handling.
We don't print <unknown> anymore in the case there is no location.
This is what the test suite expects.
The old printing logic for located items was a bit inconsistent as
it sometimes printed <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.
|
|
|
|
|
|
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 cumbersome, because now code may fail at link time if it's not
referring to the correct module name. Therefore, one has to add corresponding
open statements a the top of every file depending on a Ltac module. This
includes seemingly unrelated files that use EXTEND statements.
|
|
|
|
|
|
|
|
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.
|
|
|
|
lib/cErrors.ml)
|
|
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
|
|
|
|
|
|
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 cb6f036b8e097085a849f806aa7c2627b789bd1f.
|
|
This reverts commit 857dc0aaae30805725da213b6550dc1ff3a7adb2.
|
|
|
|
|
|
This makes the TACTIC EXTEND macro insensitive to Coq-defined arguments. They
now have to be reachable in the ML code. Note that this has some consequences,
as the previous macro was potentially mixing grammar entries and arguments as
long as their name was the same. Now, each genarg comes with its grammar
instead, so there is no way to abuse the macro.
|
|
The ARGUMENT EXTEND macro was discriminating between parsing entries known
statically, i.e. defined in Pcoq and unknown entires. Although simplifying
a bit the life of the plugin writer, it made actual interpretation difficult
to predict and complicated the code of the ARGUMENT EXTEND macro.
After this patch, all parsing entries and generic arguments used in an
ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding
a few more "open Pcoq.X" and "open Constrarg" here and there.
|
|
|
|
|
|
|
|
|
|
The previous implementation was a source of evar leaks if misused, as
it created values coming together with their current evar_map. This is
dead wrong if the value is not used on the spot. To fix this, we rather
return a ['a delayed_open] object.
Two argument types were modified: bindings and constr_bindings. The
open_constr argument should also be fixed, but it is more entangled and
thus I leave it for another commit.
|
|
|
|
|
|
The evar_map's that are used to typecheck terms must now always be
initialized with the global universe graphs using Evd.from_env, so any
failure to initialize and thread evar_map's correctly results in errors.
|
|
Some functions from pretyping/typing.ml and their derivatives were potential
source of evarmap leaks, as they dropped their resulting evarmap. This commit
clarifies the situation by renaming them according to a unsafe_* scheme. Their
sound variant is likewise renamed to their old name. The following renamings
were made.
- Typing.type_of -> unsafe_type_of
- Typing.e_type_of -> type_of
- A new e_type_of function that matches the e_ prefix policy
- Tacmach.pf_type_of -> pf_unsafe_type_of
- A new safe pf_type_of function.
All uses of unsafe_* functions should be eventually eliminated.
|
|
|
