| Age | Commit message (Collapse) | Author |
|---|
|
This makes setting the option outside of the synchronized summary impossible.
|
|
write_function
|
|
|
|
Returning a writer insinuates that it is not exactly the same as the
writer which was passed as argument, but that is incorrect.
|
|
|
|
|
|
There is little point in having a list, as there is virtually no sharing
nor expansion of bound universe names. This representation is thus more
compact.
|
|
For now this data is not stored, but the code checks that indeed the number
of names provided coincide with the instance length.
I had to reimplement the same kind of workaround hack in section handling as
the one already performed in UnivNames because the name information is not
present in the section data structure. This deserves a FIXME.
|
|
|
|
|
|
|
|
|
|
|
|
The kernel no longer has to read the configure flag, its value can now
be overriden by a coqtop/coqc argument, and more generally is easier to
set from a toplevel (such as the checker).
We also add a `-bytecode-compiler` flag.
Fixes #4607
|
|
|
|
|
|
|
|
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.
|
|
|
|
17 is a very small number as files in the stdlib will routinely pass
size 190.
As this is done only on startup, it seems wise to provide a bit more
space.
|
|
|
|
`object_name` is a particular choice of the implementation of
`Liboject`, thus it makes sense to tie it to that particular module.
This may prove useful in the future as we may want to modify object
naming.
|
|
|
|
|
|
Removing a few Global.env in the way.
|
|
|
|
It is purely functional, so no need for it to be in global now that
GlobRef.t are in the kernel.
|
|
It is purely functional, so no need for it to be in global now that
GlobRef.t are in the kernel.
Also updated the comments.
|
|
We provide a function `completion_candidates id` that will return a
list of candidates global references that have id as prefix.
This should be reasonably efficient, however UI still need to call
`shortest_qualid_of_global` which is a bit heavy. How to improve this
in the future is an open question.
cc: #7164
|
|
In general, `Nametab` is not a module you want to open globally as it
exposes very generic identifiers such as `push` or `global`.
Thus, we remove all global opens and qualify `Nametab` access. The
patch is small and confirms the hypothesis that `Nametab` access
happens in few places thus it doesn't need a global open.
It is also very convenient to be able to use `grep` to see accesses to
the namespace table.
|
|
|
|
|
|
|
|
We refactor the `Coqlib` API to locate objects over a namespace
`module.object.property`.
This introduces the vernacular command `Register g as n` to expose the
Coq constant `g` under the name `n` (through the `register_ref`
function). The constant can then be dynamically located using the
`lib_ref` function.
Co-authored-by: Emilio Jesús Gallego Arias <e+git@x80.org>
Co-authored-by: Maxime Dénès <mail@maximedenes.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
|
|
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.
|
|
Declaring the universe to the kernel/section mechanism is centralized
to [Declare.declare_universe_context].
Then the universe name object really is only about the user visible
names.
|
|
helper.
|
|
|
|
|
|
It seems these two functions don't belong there. We can remove one,
and place the other actually next to whether their semantics are
necessary.
Note that indeed the whole `Decls` file seems a bit suspicious, why we
do we register this information in a separate table instead of in the
main ones in `Lib` ?
At the suggestion of Gaëtan Gilbert we also remove unused function
`is_instance`.
|
|
Adding a ucontext to the global environment only makes sense
internally when checking a polymorphic constant.
|
|
Instead of looking into the name-oriented structure we look into the
actual section structures.
Note: together with #8475 this lets us remove UnivNames.add_global_universe.
|
|
And update documentation.
|
|
|
|
Mark boolean-valued options with :flag:
Adjust tactic and command names so parameters aren't shown in the index unless
they're needed for disambiguation.
Remove references to synchronous options.
Revise doc for tables.
Correct indentation for text below :flag:
|
|
The one in notation.ml looks trivial but is needed to do
with_notation_protection (used by inductive/fixpoint local notations).
|
|
|
|
The Dischargedhypsmap table collected the segment of section variables
that constants defined in a section were originally depending on. It
was useful to reconstruct the structure of sections as originally
given in a source file. In particular this was used in Sacerdoti
Coen's plugin for exportation of Coq files to xml. There is no
information that this plugin, moved out of Coq in September 2014, was
finally maintained, even as an external plugin. So it seems that the
Dischargedhypsmap table is virtually not used anymore in the wild.
Please contact the developers if ever the need for such a table
happens to be necessary for your work.
|
