aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs
Commit message (Collapse)AuthorAge
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-03
|\
| * Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Gravatar Hugo Herbelin2015-12-02
| |
| * Test for bug #4149.Gravatar Pierre-Marie Pédrot2015-11-30
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-29
|\|
| * Test-suite files for closed bugsGravatar Matthieu Sozeau2015-11-28
| |
| * Closed bugs.Gravatar Matthieu Sozeau2015-11-28
| |
| * Univs: entirely disallow instantiation of polymorphic constants withGravatar Matthieu Sozeau2015-11-27
| | | | | | | | | | | | | | | | | | Prop levels. As they are typed assuming all variables are >= Set now, and this was breaking an invariant in typing. Only one instance in the standard library was used in Hurkens, which can be avoided easily. This also avoids displaying unnecessary >= Set constraints everywhere.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-20
|\|
| * Fix bug #4429: eauto with arith: 70x performance regression in Coq 8.5.Gravatar Pierre-Marie Pédrot2015-11-19
| | | | | | | | | | | | | | | | | | | | | | The issue was due to the fact that unfold hints are given a priority of 4 by default. As eauto was now using hint priority rather than the number of goals produced to order the application of hints, unfold were almost always used too late. We fixed this by manually giving them a priority of 1 in the eauto tactic. Also fixed the relative order of proof depth w.r.t. hint priority. It should not be observable except for breadth-first search, which is seldom used.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-15
|\|
| * Fix bug #4412: [rewrite] (setoid_rewrite?) creates ill-typed terms.Gravatar Pierre-Marie Pédrot2015-11-12
| | | | | | | | | | We retypecheck the hypotheses introduced by the refine primitive instead of blindly trusting them when the unsafe flag is set to false.
| * Fixed test-suite file for bug #3998.Gravatar Matthieu Sozeau2015-11-12
| |
| * Now closed.Gravatar Matthieu Sozeau2015-11-11
| |
| * Fix bug #3257, setoid_reflexivity should fail if not completing the goal.Gravatar Matthieu Sozeau2015-11-11
| |
| * Fix bug #4293: ensure let-ins do not contain algebraic universes inGravatar Matthieu Sozeau2015-11-11
| | | | | | | | their type annotation.
| * Fixing bug #3554: Anomaly: Anonymous implicit argument.Gravatar Pierre-Marie Pédrot2015-11-11
| | | | | | | | | | | | | | We just handle unnamed implicits using a dummy name. Note that the implicit argument logic should still output warnings whenever the user writes implicit arguments that won't be taken into account, but I'll leave that for another time.
* | Revert "Fixing #1225: we now skip the canonically built binding contexts of"Gravatar Hugo Herbelin2015-11-10
| | | | | | | | | | | | This reverts commit 07620386b3c1b535ee7e43306a6345f015a318f0. Very sorry not ready.
* | Fixing #1225: we now skip the canonically built binding contexts ofGravatar Hugo Herbelin2015-11-10
| | | | | | | | | | | | | | | | | | the return clause and of the branches in a "match", computing them automatically when using the "at" clause of pattern, destruct, ... In principle, this is a source of incompatibilities in the numbering, since the internal binders of a "match" are now skipped. We shall deal with that later on.
* | Merge origin/v8.5 into trunkGravatar Hugo Herbelin2015-11-10
|\| | | | | | | Did some manual merge in tactics/tactics.ml.
| * Test for bug #4404.Gravatar Pierre-Marie Pédrot2015-11-10
| |
* | Merge remote-tracking branch 'origin/v8.5' into upstream-trunkGravatar Hugo Herbelin2015-11-07
|\| | | | | | | | | - Had to add a Sigma.to_evar_map - Had to rework coqdep_common.ml{,i} and coqdep.ml
| * Add test-suite file for #4273.Gravatar Matthieu Sozeau2015-11-05
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-05
|\|
| * Univs: missing checks in evarsolve with candidates and missing aGravatar Matthieu Sozeau2015-11-04
| | | | | | | | whd_evar in refresh_universes.
| * Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusionGravatar Matthieu Sozeau2015-11-04
| | | | | | | | is buggy in general.
| * Test file for #4397.Gravatar Maxime Dénès2015-11-04
| |
| * Fix bug #4151: discrepancy between exact and eexact/eassumption.Gravatar Matthieu Sozeau2015-11-02
| |
| * Refresh rigid universes as well, and in 8.4 compatibility mode,Gravatar Matthieu Sozeau2015-11-02
| | | | | | | | make them rigid to disallow minimization.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-30
|\|
| * Fixing another instance of bug #3267 in eauto, this time in theGravatar Hugo Herbelin2015-10-29
| | | | | | | | | | | | presence of hints modifying the context and of a "using" clause. Incidentally opening Hints by default in debugger.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-29
|\|
| * Univs: fix bug #4375, accept universe binders on (co)-fixpointsGravatar Matthieu Sozeau2015-10-28
| |
| * Fix bugs 4389, 4390 and 4391 due to wrong handling of universe namesGravatar Matthieu Sozeau2015-10-27
| | | | | | | | structure.
| * Two test-suite files for bugs 3974 and 3975Gravatar Pierre Letouzey2015-10-26
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-26
|\|
| * Backtracking on interpreting toplevel calls to exact in scope determinedGravatar Hugo Herbelin2015-10-24
| | | | | | | | | | | | | | | | | | | | | | | | | | by the type to prove (was introduced in 35846ec22, r15978, Nov 2012). Not only it does not work when exact is called via a Ltac definition, but, also, it does not scale easily to refine which is a TACTIC EXTEND. Ideally, one may then want to propagate scope interpretations through ltac variables, as well as supporting refine... See #4034 for a discussion.
| * Bug #3956 is fixed.Gravatar Matthieu Sozeau2015-10-21
| |
* | Removing test for bug #3956.Gravatar Pierre-Marie Pédrot2015-10-21
| | | | | | | | | | | | | | It breaks test-suite of trunk since Matthieu's fixes for the soundness of polymorphic universes, and I am unsure of the expected semantics. We should reintroduce it later on when we understand better the issue of simply fix it once and for all.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-19
|\|
| * Test for #4372 (anomaly in inversion in the presence of fake dependency).Gravatar Hugo Herbelin2015-10-19
| |
| * Test for bug #4325.Gravatar Pierre-Marie Pédrot2015-10-17
| |
* | Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-10-16
|\|
| * Test file for #4346: Set is no longer of type TypeGravatar Maxime Dénès2015-10-15
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-12
|\|
| * Adding test for bug #4366.Gravatar Pierre-Marie Pédrot2015-10-11
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-10
|\|
| * Refine fix for handling of the universe contexts of hints, depending onGravatar Matthieu Sozeau2015-10-09
| | | | | | | | their polymorphic status _and_ locality.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-09
|\|
| * Univs: fix bug #4161.Gravatar Matthieu Sozeau2015-10-08
| | | | | | | | | | Retypecheck abstracted infered predicate to register the right universe constraints.
| * Fix bug #4069: f_equal regression.Gravatar Matthieu Sozeau2015-10-07
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-01 11:53:10 +0000