| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
This brings more compatibility with handling of mutual primitive records
in the kernel.
|
| |
|
|
|
| |
This is a first step towards the acceptance of mutual record types in the
kernel.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This was completely wrong, such a term could not even be type-checked by
the kernel as it was internally using a match construct over a negative
record. They were luckily only used in upper layers, namley printing
and extraction.
Recomputing the projection body might be costly in detyping, but this only
happens when the compatibility flag is turned on, which is not the default.
Such flag is probably bound to disappear anyways.
Extraction should be fixed though so as to define directly primitive
projections, similarly to what has been done in native compute.
|
| |/
|
|
|
|
| |
This field used to signal that a constant was the compatibility
eta-expansion of a primitive projections, but since a previous cleanup in
the kernel it had become useless.
|
| |
|
|
| |
We move the last 3 types to more adequate places.
|
| |
|
|
|
| |
Instead of having the projection data in the constant data we have it
independently in the environment.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
In #6092, `global_reference` was moved to `kernel`. It makes sense to
go further and use the current kernel style for names.
This has a good effect on the dependency graph, as some core modules
don't depend on library anymore.
A question about providing equality for the GloRef module remains, as
there are two different notions of equality for constants. In that
sense, `KerPair` seems suspicious and at some point it should be
looked at.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
The `reference` type contains some ad-hoc locations in its
constructors, but there is no reason not to handle them with the
standard attribute container provided by `CAst.t`.
An orthogonal topic to this commit is whether the `reference` type
should contain a location or not at all.
It seems that many places would become a bit clearer by splitting
`reference` into non-located `reference` and `lreference`, however
some other places become messier so we maintain the current status-quo
for now.
|
| |\
| |
| |
| | |
wish #4129)
|
| | |
| |
| |
| |
| |
| | |
Attempt to extract the current ongoing proof (request by
Clément Pit-Claudel on coqdev, and also #4129).
Evars are handled as axioms.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This is a bit artificial since the extraction normally operates on
finished constrs (with no evars). But:
- Since we use Retyping quite a lot, switching to EConstr.t allows
to get rid of many `EConstr.Unsafe.to_constr (... (EConstr.of_constr ...))`
- This prepares the way for a possible extraction of the content
of ongoing proofs (a forthcoming `Show Extraction` command, see #4129 )
|
| | | |
|
| |/ |
|
| |
|
|
| |
longer use camlp4.
|
| |
|
|
|
|
|
|
| |
Unfortunately OCaml doesn't deprecate the constructors of a type when
the type alias is deprecated.
In this case it means that we don't get rid of the kernel dependency
unless we deprecate the constructors too.
|
| | |
|
| | |
|
| |\ |
|
| | | |
|
| |\ \
| | |
| | |
| | | |
constructs.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
Extending terms is notoriously difficult. We try to get more help from
the compiler by making sure such an extension will trigger non
exhaustive pattern matching warnings.
|
| | | | |
|
| | |/ |
|
| |/
|
|
|
|
| |
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.
|
| |\ |
|
| | |
| |
| |
| | |
We do up to `Term` which is the main bulk of the changes.
|
| |/
|
|
| |
Fixes #6022.
|
| |
|
|
|
| |
Compared to the original proposition (01f848d in #960), this commit
only changes files containing bug numbers that are also PR numbers.
|
| |\
| |
| |
| | |
Compute plugin
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
BZ#4852)
This code simplification isn't that important, but it can trigger further
simplifications elsewhere, see for instance BZ#4852.
NB: normally, the extraction favors eta-expanded forms, since that's the usual
way to avoid issues about '_a type variables that cannot be generalized. But
the atomic eta-reductions done here shouldn't be problematic (no applications
put outside of functions).
|
| |/
|
|
| |
See https://github.com/letouzey/extraction-compute for more details
|
| |
|
|
|
| |
The old algorithm was relying on list membership, which is O(n). This was
nefarious for terms with many binders. We use instead sets in O(log n).
|
| |\
| |
| |
| | |
work better on them
|
| | |
| |
| |
| |
| |
| |
| |
| | |
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).
|
| |/ |
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| | | | | |
|
| | |_|/
|/| | |
|
| |\ \ \
| |_|/
|/| |
| | | |
4844 and 4824)
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |\ \ |
|
| |\ \ \ |
|
Pierre-Marie Pédrot
Enrico Tassi
Maxime Dénès
Emilio Jesus Gallego Arias
Gaëtan Gilbert
Hugo Herbelin
Pierre Letouzey
Vincent Laporte
Théo Zimmermann
Jim Fehrle
Paul Steckler
Paul Steckler
Tej Chajed
Matej Košík