| Age | Commit message (Collapse) | Author |
|---|
|
"Declaration" hooks can be polymorphic on their return type, however
this facility doesn't seem used in the codebase.
We thus remove the polymorphism with the hope to be able to reify the
control later on.
|
|
These hooks are 10-years old and long unused I think.
|
|
|
|
|
|
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>
|
|
|
|
A few of them will be of help for future cleanups. We have spared the
stuff in `Names` due to bad organization of this module following the
split from `Term`, which really difficult things removing the
constructors.
|
|
|
|
|
|
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.
|
|
helper.
|
|
Mostly via `dev/tools/update-compat.py --cur-version=8.9`
We just remove test-suite/success/FunindExtraction_compat86.v because,
except for the `Extraction iszero.` line at the bottom, it is a
duplicate of `test-suite/success/Funind.v` (except with `-compat 8.6`).
We also manually update a number of test-suite files to pre-emptively
remove compatibility notations (which used to be compat 8.6, but are now
compat 8.7).
|
|
This was imposing a bit of useless burden on the API for no good reason.
|
|
|
|
|
|
|
|
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`.
|
|
`Classes.new_instance` is one of the largest functions of the
codebase; we split it up and reduce indentation.
This will help further cleanups. This PR should introduce no code
changes other than splitting the function up.
|
|
This shall eventually allow to call Himsg at any point of the
execution, independently of the exact current global environment.
|
|
|
|
This was introduced in #7820 and it is not needed indeed. As 8.9 was
not released we don't need to perform a deprecation phase.
|
|
|
|
|
|
It was working in very specific context of section variables. We make
it work similarly in the same kind of specific context of
Parameters. See test file SchemeEquality.v for the expected form. See
discussion at PR #8509.
|
|
|
|
|
|
We raise a normal error instead of an anomaly.
|
|
We raise a normal error instead of an anomaly.
This fixes also #2550, #8492.
Note in passing: While the case of a type "Inductive I := list I -> I"
is difficult, the case of a "Inductive I := list nat -> I" should be
easily doable.
|
|
|
|
Closes #7380. Ubuntu 18.04 and Debian Buster will ship this OCaml
version so it makes sense we bump our dependency to 4.05.0 as we can
use some newer compiler features.
|
|
|
|
|
|
|
|
And update documentation.
|
|
We missed two more constructor / record deprecation.
|
|
|
|
The regression was introduced in 1522b989 (PR #7193) which itself was
fixing bug #7192. (Note another regression of the same commit which is
fixed in #8416.)
|
|
|
|
|
|
When deprecating some type alias [due to code refactoring] we forgot
to deprecate the constructors too. Closes #8498.
|
|
In particular we check if really used for internal debugging purpose
or to display a message to the user. In the latter case, we replace it
(when possible) by a higher-level printer (e.g. printing foo instead
of Top.foo). In the former case, we clarify that the use is a
debugging use.
Still not perfect (see a few FIXME).
|
|
We simply declare the bound universes with their user-facing name in the
evarmap and call all printing functions on uninstantiated terms. We had to
tweak the universe name declaring function so that it would work properly
with bound universe variables and handle sections correctly.
This changes the output of polymorphic definitions with unnamed universe
variables. Now they are printed as Var(i) instead of the Module.n uid
that came from their absolute name.
|
|
Switch to using exceptions rather than user errors. This will be
required because the machinery for printing constrs is not available in
notation.ml, so we move the error message printing to himsg.ml instead.
This is commit 2/4 in the fix for #8401.
|
|
|
|
|
|
|
|
|
|
|
|
eg in [Class Foo (A:Type) := foo : A.] the universe should be
declared when declaring the constant [Foo] and not [foo].
|
|
|
