aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Expand)Author
2015-12-17(Partial) fix for bug #4453: raise an error instead of an anomaly.Matthieu Sozeau
2015-12-17Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-15Extraction: more cautious use of intermediate result caching (fix #3923)Pierre Letouzey
2015-12-15Fix test-suite files after change in refine tactic.Maxime Dénès
2015-12-15Refine tactic now shelves unifiable holes.Pierre-Marie Pédrot
2015-12-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-14Test file for #4363 was not complete.Maxime Dénès
2015-12-11Univs: Fix bug #4363, nested abstract.Matthieu Sozeau
2015-12-08Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-03Univs: fix bug #4443.Matthieu Sozeau
2015-12-03Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-02Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Hugo Herbelin
2015-11-30Test for bug #4149.Pierre-Marie Pédrot
2015-11-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-28Test-suite files for closed bugsMatthieu Sozeau
2015-11-28Closed bugs.Matthieu Sozeau
2015-11-27Univs: entirely disallow instantiation of polymorphic constants withMatthieu Sozeau
2015-11-20Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-19Fix bug #4429: eauto with arith: 70x performance regression in Coq 8.5.Pierre-Marie Pédrot
2015-11-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-12Fix bug #4412: [rewrite] (setoid_rewrite?) creates ill-typed terms.Pierre-Marie Pédrot
2015-11-12Fixed test-suite file for bug #3998.Matthieu Sozeau
2015-11-11Now closed.Matthieu Sozeau
2015-11-11Fix bug #3257, setoid_reflexivity should fail if not completing the goal.Matthieu Sozeau
2015-11-11Fix bug #4293: ensure let-ins do not contain algebraic universes inMatthieu Sozeau
2015-11-11Fixing bug #3554: Anomaly: Anonymous implicit argument.Pierre-Marie Pédrot
2015-11-10Revert "Fixing #1225: we now skip the canonically built binding contexts of"Hugo Herbelin
2015-11-10Fixing #1225: we now skip the canonically built binding contexts ofHugo Herbelin
2015-11-10Merge origin/v8.5 into trunkHugo Herbelin
2015-11-10Test for bug #4404.Pierre-Marie Pédrot
2015-11-07Merge remote-tracking branch 'origin/v8.5' into upstream-trunkHugo Herbelin
2015-11-05Add test-suite file for #4273.Matthieu Sozeau
2015-11-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-04Univs: missing checks in evarsolve with candidates and missing aMatthieu Sozeau
2015-11-04Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusionMatthieu Sozeau
2015-11-04Test file for #4397.Maxime Dénès
2015-11-02Fix bug #4151: discrepancy between exact and eexact/eassumption.Matthieu Sozeau
2015-11-02Refresh rigid universes as well, and in 8.4 compatibility mode,Matthieu Sozeau
2015-10-30Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-29Fixing another instance of bug #3267 in eauto, this time in theHugo Herbelin
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-28Univs: fix bug #4375, accept universe binders on (co)-fixpointsMatthieu Sozeau
2015-10-27Fix bugs 4389, 4390 and 4391 due to wrong handling of universe namesMatthieu Sozeau
2015-10-26Two test-suite files for bugs 3974 and 3975Pierre Letouzey
2015-10-26Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-24Backtracking on interpreting toplevel calls to exact in scope determinedHugo Herbelin
2015-10-21Bug #3956 is fixed.Matthieu Sozeau
2015-10-21Removing test for bug #3956.Pierre-Marie Pédrot
2015-10-19Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-19Test for #4372 (anomaly in inversion in the presence of fake dependency).Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 05:32:53 +0000