| Commit message (Collapse) | Author | Age |
|---|
| |\
| |
| |
| | |
anonymous variables)
|
| | |
| |
| |
| |
| | |
As explained in BZ#5713 report, the requirement for a non-empty
context is not needed, so we remove it.
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | | | | | |
|
| | |_|/ /
|/| | |
| | | |
| | | |
| | | | |
The code generating the projection was unconditionally generating
pattern-matchings, although this is incorrect for primitive records.
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
restructuration
|
| |\ \ \ \ \ |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This reverts commit 53a50875 and a bit more: it also makes the check
for possibly ignoring formatting spaces irrelevant, since the previous
commit makes that curly brackets are not any more dropped for
printing.
|
| | |/ / / /
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
- Formerly, notations such as "{ A } + { B }" were typically split
into "{ _ }" and "_ + _". We keep the split only for parsing, which
is where it is really needed, but not anymore for interpretation,
nor printing.
- As a consequence, one notation string can give rise to several
grammar entries, but still only one printing entry.
- As another consequence, "{ A } + { B }" and "A + { B }" must be
reserved to be used, which is after all the natural expectation,
even if the sublevels are constrained.
- We also now keep the information "is ident", "is binder" in the
"key" characterizing the level of a notation.
|
| | |/ / /
|/| | | |
|
| | |/ /
|/| | |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | | | | | |
|
| | |_|/ /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This is a second try at removing the hooks for the legacy xml export
system which can't currently be tested.
It is also not included in the API, so it should either be included in
it or this PR be applied.
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \ |
|
| | |_|_|_|/ /
|/| | | | | |
|
| | |_|/ / /
|/| | | | |
|
| | | | | | |
|
| | |/ / /
|/| | | |
|
| |/ / /
| | |
| | |
| | | |
TestCompile)
|
| |\ \ \
| | | |
| | | |
| | | | |
4844 and 4824)
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
4844 and 4824)
The commit 8e257d4 (which consider the dummy type Tdummy to be polymorphic and hence
immune of the need for unsafeCoerce) is quite wrong, even if in pratice it worked ok
most of the time. The confusion comes from the fact that the dummy value (__ aka MLdummy
internally) is implemented in Haskell as Prelude.error, hence it has indeed a polymorphic
unrestricted type. But the dummy type Tdummy used when extracting types must be monomorphic
(otherwise type parameters would have to be propagated out of any type definition involving
Tdummy). We implement Tdummy by Haskell's (), which for instance isn't convertible to Any,
as shown by the examples in bug reports 4844 and 4824.
This fix will bring back some more unsafeCoerce in Haskell extraction, including possibly
a few spurious ones. And these extra unsafeCoerce might also hinder further code optimisations.
We tried to mitigate that by directly removing [MLmagic] constructors in front of [MLdummy _].
NB: even if the original bug report mentions universe polymorphism, this issue is
almost unrelated to it. It just happens that when universe polymorphism is off,
an inductive instance is fully placed in Prop (cf. template polymorphism) in the example,
avoiding triggering the issue.
Warning: the test-suite file is there for archiving the repro case, but currently it doesn't
test much (we should run ghc on the extracted code).
|
| |/ / /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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).
|
| | | |
| | |
| | |
| | |
| | | |
I had to slightly tweak a test in order to work around a bug of simpl that
loses universes constraints when refolding polymorphic fixpoints.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The function turning a side-effect declaration into the corresponding
entry was crazily wrong, as it used a named universe context quantifying
over DeBruijn universe indices. Declaring such entries resulted
in random anomalies.
This fixes bug #5641.
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | | | | | |
|
| | |_|/ /
|/| | | |
|
| |\| | | |
|
| |\ \ \ \ |
|
| | |/ / /
|/| | | |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| | | | | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
Ltac pattern-matching was requiring dependent variables to be named.
This "natural" expectation is however not guaranteed by unification:
an evar can be dependent on an anonymous variable, resulting in
elaborated terms with dependent anonymous variables (see example in
file 5434.v).
This commit "fixes" the problem by not requiring that dependent
variables are named in ltac pattern-matching. Ltac pattern-matching
names itself these anonymous dependent variables, using the same
strategy as the printer (i.e. using "H" to display such
internally-anonymous dependent variables).
|
| | |_|_|_|/
|/| | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | | |
Fix a mistake in record declaration
|
| |/ / / / |
|
| | | | |\ |
|
| |\ \ \ \ \ |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
In the previous setting, all plugins/ltac/*.cmxs except ltac_plugin.cmxs
(for instance coretactics.cmxs, g_auto.cmxs, ...) were utterly bogus :
- wrong -for-pack used for their inner .cmx
- dependency over modules not provided (for instance Tacenv, that ends
up being a submodule of the pack ltac_plugin).
But we were lucky, those files were actually never loaded, thanks to the
several DECLARE PLUGIN inside coretactics and co, that end up in ltac_plugin,
and hence tell Coq that these modules are already known, preventing
any attempt to load them.
Anyway, this commit cleans up this mess (thanks PMP for the help)
|
| |\ \ \ \ \ \
| |_|_|/ / /
|/| | | | | |
|
| |\ \ \ \ \ \ |
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
sorting for the dependency order option.
|
Maxime Dénès
Hugo Herbelin
Pierre-Marie Pédrot
Matthieu Sozeau
Théo Zimmermann
Emilio Jesus Gallego Arias
Julien Forest
Pierre Letouzey
Gaëtan Gilbert
Amin Timany
Matthieu Sozeau