| Age | Commit message (Collapse) | Author |
|---|
|
I believe this renaming makes it easier for new contributors to discover
the code of `ring`.
|
|
Add headers to a few files which were missing them.
|
|
Previously, they were using a map that was different from the one used
by the real lookup, leading to confusing information (number of
instances could be wrong, etc).
|
|
|
|
reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.
We remove the reference type and replace its uses by qualid.
|
|
Unfortunately, mli-only files cannot be included in packs, so we have
the weird situation that the scope for `Tacexpr` is wrong. So we
cannot address the module as `Ltac_plugin.Tacexpr` but it lives in the
global namespace instead.
This creates problem when using other modular build/packing strategies
[such as #6857] This could be indeed considered a bug in the OCaml
compiler.
In order to remedy this situation we face two choices:
- leave the module out of the pack (!)
- create an implementation for the module
I chose the second solution as it seems to me like the most sensible
choice.
cc: #6512.
|
|
|
|
We do up to `Term` which is the main bulk of the changes.
|
|
|
|
|
|
|
|
The ring ASTs were put in a separate interface, and only the
extension-related code was put in a dedicated G_newring file.
|
