| Age | Commit message (Collapse) | Author |
|---|
|
We move `Declaremods` to the vernac layer as it implement
vernac-specific logic to manipulate modules which moreover is highly
imperative.
This forces code [such as printing] to manipulate the _global
imperative_ state which is a bit fishy.
The key improvement in this PR is that now `Global` is not used
anymore in `library`, so we can proceed to move it upwards.
This move is a follow-up of #10562 and a step towards moving `Global`
upper, likely to `interp` in the short term.
|
|
|
|
|
|
|
|
This should compensate the removal of the library-level optimization,
while maintaining correct behavior.
|
|
They have been already cached at loading time.
|
|
`Import` does not actually need to register an object, only `Export`
does. So we specialize and rename the object into `ExportObject`.
|
|
|
|
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
We make a few libobject constructions (Module, Module Type,
Include,...) first-class and rephrase their handling in direct style (removing
the inversion of control). This makes it easier to define iterators over
objects without hacks like inspecting the tags of dynamic objects.
|
|
|
|
Instead we get the symbols from a Environ.env.
We make them accessible to the produced code through a reference
managed by the kernel, similar to the return values except inverting
when it's written and when it's read.
|
|
|
|
|
|
|
|
We move `object_prefix` to `Nametab`. This highlights the coupling of
`Lib` and `Nametab` wrt naming.
This also thins `Libname`, which IMHO is a good thing as we are
talking about "local, internal" naming here.
|
|
This type is "private" to the Nametab, which manages it. It thus makes
sense IMHO to live there.
|
|
We remove sections paths from kernel names. This is a cleanup as most of the times this information was unused. This implies a change in the Kernel API and small user visible changes with regards to tactic qualification. In particular, the removal of "global discharge" implies a large cleanup of code.
Additionally, the change implies that some machinery in `library` and `safe_typing` must now take an `~in_section` parameter, as to provide the information whether a section is open or not.
|
|
|
|
|
|
Morally, `library` should not depend on the vernacular
definition. This will also create problems when trying to modularize
the codebase due to the cycle [vernacs depend for example on
constrexprs].
The fix is fortunately easy.
|
|
|
|
We follow the suggestions in #402 and turn uses of `Loc.located` in
`vernac` into `CAst.t`. The impact should be low as this change mostly
affects top-level vernaculars.
With this change, we are even closer to automatically map a text
document to its AST in a programmatic way.
|
|
We defer the computation of the universe quantification to the upper layer,
outside of the kernel.
|
|
This is a minor cleanup adding a record in a try to structure the
state living in `Lib`.
|
|
We deprecate a few functions that were deprecated in the comments plus
we place `Nameops` and `Univops` in engine where they do seem to
belong in the large picture of code organization.
|
|
This will allow to merge back `Names` with `API.Names`
|
|
This is a second try at removing the hooks for the legacy xml export
system which can't currently be tested.
It is also not included in the API, so it should either be included in
it or this PR be applied.
|
|
|
|
AFAICS this function predates modern state-handling; nowadays
summaries are stored by the STM and nobody were using this
information.
|
|
As per https://github.com/coq/coq/pull/716#issuecomment-305140839
Partially using
```bash
git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i
```
and
```bash
git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i
```
The rest were manually edited by looking at the results of
```bash
git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less
```
|
|
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.
|
|
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.
|
|
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
|
This add LtacProfiling. Much of the code was written by Tobias Tebbi
(@tebbi), and Paul A. Steckler was invaluable in porting the code to Coq
v8.5 and Coq trunk.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
As shown by the code snippets in these bug reports, I've been too
hasty in considering these situations as anomalies in commit 466c4cb
(at least the one at the last line of consistency_checks). So let's turn
these anomalies back to regular user errors, as they were before this commit.
|
|
Fixes #4139 (Not_found exception with Require in modules).
|
|
Since error messages are ultimately passed to Format, which has its own
buffers for concatenating strings, using concatenation for preparing error
messages just doubles the workload and increases memory pressure.
|
|
This reverts commit 6d5b56d971506dfadcfc824bfbb09dc21718e42b but does not put
back in place the Requires inside modules that were found in the std lib.
Conflicts:
kernel/safe_typing.ml
|
|
|
|
After this commit, module_type_body is a particular case of module_type.
For a [module_type_body], the implementation field [mod_expr] is
supposed to be always [Abstract]. This is verified by coqchk, even
if this isn't so crucial, since [mod_expr] is never read in the case
of a module type.
Concretely, this amounts to the following rewrite on field names
for module_type_body:
- typ_expr --> mod_type
- typ_expr_alg --> mod_type_alg
- typ_* --> mod_*
and adding two new fields to mtb:
- mod_expr (always containing Abstract)
- mod_retroknowledge (always containing [])
This refactoring should be completely transparent for the user.
Pros: code sharing, for instance subst_modtype = subst_module.
Cons: a runtime invariant (mod_expr = Abstract) which isn't
enforced by typing. I tried a polymorphic typing of mod_expr,
to share field names while not having mtb = mb, but the OCaml
typechecker isn't clever enough with polymorphic mutual fixpoints,
and reject code sharing (e.g. between subst_modtype and subst_module).
In the future (with ocaml>=4), some GADT could maybe help here,
but for now the current solution seems good enough.
|
