| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | |
| | | |
| | | |
| | | | |
linking chain.
|
| | |_|/
|/| |
| | |
| | | |
This removes a dependency from `G_vernac` to `Metasyntax`.
|
| | | | |
|
| | |/
|/|
| |
| |
| |
| |
| |
| | |
As explained in edf85b9, the original commit that merged the module_body
and module_type_body representations, this was delayed to a later time
assumedly due to OCaml lack of GADTs. Actually, the only thing that was
needed was polymorphic recursion, which has been around already for a
relatively long time (since 3.12).
|
| | | |
|
| |\ \ |
|
| |\ \ \
| | | |
| | | |
| | | | |
restructuration
|
| |\ \ \ \ |
|
| | |/ / /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This allows to issue a more appropriate message when a notation with a
{ } cannot be defined because of an incompatible level. E.g.:
Notation "{ A } + B" := (sumbool A B) (at level 20).
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
with OCaml.
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \ |
|
| | |_|/ / / /
|/| | | | |
| | | | | |
| | | | | |
| | | | | | |
Indeed OCaml has a similar file and this conflicts, at least in
debugger.
|
| | |_|_|_|/
|/| | | | |
|
| | | | | | |
|
| | | | | | |
|
| | |/ / /
|/| | |
| | | |
| | | | |
This was already the case, but the API was not exposing this.
|
| | |_|/
|/| | |
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
We now only issue an error for locally specified (non)cumulativity
whenever it is the context (set locally or globally) is monorphic.
|
| |\ \ \ \
| |_|/ /
|/| | | |
|
| | |_|/
|/| | |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| | |_|_|/ /
|/| | | | |
|
| | |_|_|/
|/| | | |
|
| | | |/
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The use of template polymorphism in constants was quite limited, as it
only applied to definitions that were exactly inductive types without any
parameter whatsoever. Furthermore, it seems that following the introduction
of polymorphic definitions, the code path enforced regular polymorphism as
soon as the type of a definition was given, which was in practice almost
always.
Removing this feature had no observable effect neither on the test-suite,
nor on any development that we monitor on Travis. I believe it is safe to
assume it was nowadays useless.
|
| | |/
|/|
| |
| |
| | |
We use an algebraic type instead of a pair of a boolean and the corresponding
data. For now, this is isomorphic, but this allows later change in the structure.
|
| |\ \ |
|
| |\ \ \ |
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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`
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We sort the dependency graph of API by following a logical declaration
order in `API.{ml,mli}` related to the actual dependency order of Coq
modules.
Things are a bit tricky here as Coq itself relies on the fact that
OCaml treats module interface and implementation separately
dependency-wise; however, when resorting module alias the design seems
to become more coupled.
Currently, API exposes both "namespaces", asserting a large number of
type equality between them, however the `API` namespace is not
self-contained.
In particular, this is a first step to solve problems such as
`Summary.frozen` being used in `API.mli` but not declared by the
`API.Summary` module, etc... In general we follow the invariant that a
type used in `API` must have been declared before.
Keep in mind that OCaml upstream has warned that it maybe tricky to
alias objects in this way. In particular, after API the old `mli` only
files have become full compilation units so we may want to be more
careful here.
The more "correct" declaration order allows us to remove the
`API.Prelude` module, as well as some other declarations that I
consider as spurious.
We still maintain the large number of type aliases which will be
removed in a future patch.
We follow linking order except for files in `intf`, which are
conceptually wrongly placed in the linking hierarchy but this doesn't
matter as the files don't contain any implementation.
We also move a couple of `.mli` only files to `.ml` so we are
consistent, and correct their linking order in `mllib`, even if that
doesn't matter as such `.ml`-only files contain no implementations.
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Avoid Anomaly (or Assert False) when a module signature contains
an applied functor followed by a "with Definition" or "with Module"
Also fix the dependency computation in presence of a "with Definition"
Concerning 4720, the code extracted out of this bug report was suboptimal
in Coq 8.4 (it was compilable, but could have probably been tweaked into a
real issue producing faulty code).
But the example of 4720 (and some variants of it) was broken since 8.5,
for the same reasons as 5177 and 5240. And the good news is that after
these repairs, the example of bug 4720 is now extracted to correct code
(the "with" is preserved).
|
| |\ \ |
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | | |
This essentially means storing the abstract universe context in the typeclass
data, and abstracting it when necessary.
|
| | | |
| | |
| | |
| | |
| | | |
We aditionally return the abstract universe context inside the option. This
is relatively painless as most uses were using the option as a boolean.
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | | |
`VernacStartTheoremProof` contained a stale bool parameter from 15
years ago, which is unused today.
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \ |
|
| | |_|_|/ / /
|/| | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This is necessary in order for clients to identify the results of
queries. This is a minor breaking change of the protocol, affecting
only this particular call.
This change is necessary in order to fix bug ####.
|
| | |_|/ / /
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Unluckily, this forces replacing a lot of code in plugins, because the API
defined the type of goals and tactics in Proof_type, and by the no-alias rule,
this was the only one. But Proof_type was already implicitly deprecated, so
that the API should have relied on Tacmach instead.
|
| | | | | | |
|
Emilio Jesus Gallego Arias
Pierre-Marie Pédrot
Maxime Dénès
Hugo Herbelin
Sigurd Schneider
Amin Timany
amblaf
Matej Košík
Pierre Letouzey