aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs
Commit message (Collapse)AuthorAge
* Merge PR #916: Fixing notation bug 5608 involving { } and a slight ↵Gravatar Maxime Dénès2017-08-29
|\ | | | | | | restructuration
* \ Merge PR #773: [flags] Remove XML output flag.Gravatar Maxime Dénès2017-08-29
|\ \
| | * Dropping former fix to bug #5469 (notation format not recognizing curly braces).Gravatar Hugo Herbelin2017-08-29
| | | | | | | | | | | | | | | | | | | | | 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.
| | * A little reorganization of notations + a fix to #5608.Gravatar Hugo Herbelin2017-08-29
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | | | - 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.
* | Merge PR #942: solving b1859Gravatar Maxime Dénès2017-08-16
|\ \
* \ \ Merge PR #841: Timorous fix of bug #5598 on global existing class in sectionsGravatar Maxime Dénès2017-08-16
|\ \ \
| | * | Adding a test for BZ#1859 as suggested by @tchajed.Gravatar Théo Zimmermann2017-08-15
| | | |
| | | * [flags] Remove XML output flag.Gravatar Emilio Jesus Gallego Arias2017-08-01
| |_|/ |/| | | | | | | | | | | | | | | | | | | | 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.
* | | Merge PR #928: Fixing bug #5671 (tactic specialize unclean wrt Metas).Gravatar Maxime Dénès2017-08-01
|\ \ \
* \ \ \ Merge PR #926: test-suite uses Extraction TestCompileGravatar Maxime Dénès2017-08-01
|\ \ \ \
* \ \ \ \ Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709)Gravatar Maxime Dénès2017-08-01
|\ \ \ \ \
* | | | | | closing bug 5315Gravatar Julien Forest2017-07-29
| |_|_|_|/ |/| | | |
| | | * | Fixing bug #5671 (specialize unclean wrt Metas).Gravatar Hugo Herbelin2017-07-27
| |_|/ / |/| | |
| | * | test-suite: more use of the new command Extraction TestCompileGravatar Pierre Letouzey2017-07-27
| | | |
| | * | Enrich test file 4720.v with a compilation test of the extracted codeGravatar Pierre Letouzey2017-07-26
| |/ / |/| |
| * | adding a test-suite file 4709.v (thanks to the new command Extraction ↵Gravatar Pierre Letouzey2017-07-26
|/ / | | | | | | TestCompile)
* | Merge PR #918: Extraction: do not mix Haskell types Any and () (fix bugs ↵Gravatar Maxime Dénès2017-07-26
|\ \ | | | | | | | | | 4844 and 4824)
| * | Extraction: do not mix Haskell types Any and () (revert 8e257d4, fix bugs ↵Gravatar Pierre Letouzey2017-07-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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).
* | | Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720)Gravatar Pierre Letouzey2017-07-20
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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).
* | Removing the uses of abstraction-breaking code in Lemmas.Gravatar Pierre-Marie Pédrot2017-07-13
| | | | | | | | | | I had to slightly tweak a test in order to work around a bug of simpl that loses universes constraints when refolding polymorphic fixpoints.
* | Fix nonsensical universe abstraction in the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | | | | | | | | | | | | | | 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.
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\ \
* \ \ Merge PR#843: closing bug #5618 introduce by PR 828Gravatar Maxime Dénès2017-06-30
|\ \ \
| * | | closing bug #5618 introduce by PR 828Gravatar Julien Forest2017-06-29
| | | |
| | | * A fix for #5598 (no discharge of Existing Classes referring to local variables).Gravatar Hugo Herbelin2017-06-28
| |_|/ |/| |
* | | Merge PR#828: closing bug #4250Gravatar Maxime Dénès2017-06-26
|\| |
* | | Merge PR#794: Cleanup of ltac cmxsGravatar Maxime Dénès2017-06-23
|\ \ \
| | * | closing bug #4250Gravatar Julien Forest2017-06-23
| |/ / |/| |
* | | Merge PR#787: [typeclasses eauto] Fix bug #3943: non-termination in topologicalGravatar Maxime Dénès2017-06-19
|\ \ \
* \ \ \ Merge PR#613: Cumulativity for inductive typesGravatar Maxime Dénès2017-06-19
|\ \ \ \
* | | | | Test case for bug 5578.Gravatar Maxime Dénès2017-06-19
| | | | |
* | | | | Increase the time limit on 4366.v to make gitlab work better.Gravatar Gaëtan Gilbert2017-06-16
| | | | |
| * | | | Disable debug printingGravatar Amin Timany2017-06-16
| | | | | | | | | | | | | | | | | | | | Fix a mistake in record declaration
| * | | | Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
|/ / / /
| | | * Merge PR#440: Univs: fix bug #5365, generation of u+k <= v constraintsGravatar Maxime Dénès2017-06-15
| | | |\
* | | | \ Merge PR#719: Constrexpr.Numeral without bigintGravatar Maxime Dénès2017-06-15
|\ \ \ \ \
| | | * | | plugins/ltac : avoid spurious .cmxs filesGravatar Pierre Letouzey2017-06-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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)
* | | | | | Merge PR#375: DeprecationGravatar Maxime Dénès2017-06-15
|\ \ \ \ \ \ | |_|_|/ / / |/| | | | |
* | | | | | Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Maxime Dénès2017-06-14
|\ \ \ \ \ \
| | | | * | | [typeclasses eauto] Fix bug #3943: non-termination in topologicalGravatar Matthieu Sozeau2017-06-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | sorting for the dependency order option.
* | | | | | | Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
| |_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted.
| | | * | | Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Gravatar Pierre Letouzey2017-06-14
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | This string contains the base-10 representation of the number (big endian) Note that some inner parsing stuff still uses bigints, see egramcoq.ml
| | * | | Remove support for Coq 8.4.Gravatar Guillaume Melquiond2017-06-14
| |/ / / |/| | |
| * | | A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Hugo Herbelin2017-06-09
|/ / / | | | | | | | | | | | | | | | | | | | | | | | | Also taking into account a name in the return clause and in the indices. Note the double meaning ``bound as a term to match'' and ``binding in the "as" clause'' when the term to match is a variable for all of "match", "if" and "let".
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\ \ \
| | * | Adding a test case as requested in bug 5205.Gravatar Théo Zimmermann2017-06-08
| |/ /
* | | Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a ↵Gravatar Maxime Dénès2017-06-06
|\ \ \ | | | | | | | | | | | | short econstr-cleaning of record.ml
| | | * Univs: fix bug #5365, generation of u+k <= v constraintsGravatar Matthieu Sozeau2017-06-05
| | | | | | | | | | | | | | | | Use an explicit label ~algebraic for make_flexible_variable as well.
| | * | Merge PR#705: Fix bug #5019 (looping zify on dependent types)Gravatar Maxime Dénès2017-06-02
| | |\ \
| | * \ \ Merge PR#631: Fix bug #5255Gravatar Maxime Dénès2017-06-01
| | |\ \ \