aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed
AgeCommit message (Collapse)Author
2015-11-10Fixing #1225: we now skip the canonically built binding contexts ofHugo Herbelin
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.
2015-11-10Merge origin/v8.5 into trunkHugo Herbelin
Did some manual merge in tactics/tactics.ml.
2015-11-10Test for bug #4404.Pierre-Marie Pédrot
2015-11-07Merge remote-tracking branch 'origin/v8.5' into upstream-trunkHugo Herbelin
- Had to add a Sigma.to_evar_map - Had to rework coqdep_common.ml{,i} and coqdep.ml
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
whd_evar in refresh_universes.
2015-11-04Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusionMatthieu Sozeau
is buggy in general.
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
make them rigid to disallow minimization.
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
presence of hints modifying the context and of a "using" clause. Incidentally opening Hints by default in debugger.
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
structure.
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
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.
2015-10-21Bug #3956 is fixed.Matthieu Sozeau
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
2015-10-17Test for bug #4325.Pierre-Marie Pédrot
2015-10-16Merge branch 'v8.5' into trunkMaxime Dénès
2015-10-15Test file for #4346: Set is no longer of type TypeMaxime Dénès
2015-10-12Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-11Adding test for bug #4366.Pierre-Marie Pédrot
2015-10-10Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-09Refine fix for handling of the universe contexts of hints, depending onMatthieu Sozeau
their polymorphic status _and_ locality.
2015-10-09Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-08Univs: fix bug #4161.Matthieu Sozeau
Retypecheck abstracted infered predicate to register the right universe constraints.
2015-10-07Fix bug #4069: f_equal regression.Matthieu Sozeau
2015-10-07Univs: add Strict Universe Declaration option (on by default)Matthieu Sozeau
This option disallows "declare at first use" semantics for universe variables (in @{}), forcing the declaration of _all_ universes appearing in a definition when introducing it with syntax Definition/Inductive foo@{i j k} .. The bound universes at the end of a definition/inductive must be exactly those ones, no extras allowed currently. Test-suite files using the old semantics just disable the option.
2015-10-06Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-06Fix bug #4354: interpret hints in the right env and sigma.Matthieu Sozeau
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Univs: fix test-suite file for #4287, now properly rejected.Matthieu Sozeau
2015-10-02Univs: Remove test-suite file #3309Matthieu Sozeau
This relied on universes lower than Prop. A proper test for the sharing option should be found, -type-in-type is not enough either.
2015-10-02Univs: fix test-suite file (4301 is invalid, but a good regression test)Matthieu Sozeau
2015-10-02Univs: correct handling of with in modulesMatthieu Sozeau
For polymorphic and non-polymorphic parameters and definitions, fixes bugs #4298, #4294
2015-10-02Univs: fix bug #4251, handling of template polymorphic constants.Matthieu Sozeau
2015-10-02Univs: fixed 3685 by side-effect :)Matthieu Sozeau
2015-10-02Univs: minor fixes to test-suite filesMatthieu Sozeau
108 used an implicit lowering to Prop.
2015-10-02Univs: fix test-suite file for HoTT/coq bug #120Matthieu Sozeau
2015-10-02Univs: test-suite file for bug #2016Matthieu Sozeau
2015-10-02Univs: test-suite file for #4301, subtyping of poly parametersMatthieu Sozeau
2015-10-02Fix test-suite file for bug #3777Matthieu Sozeau
2015-10-02Fix test-suite file: failing earlier as expected.Matthieu Sozeau
2015-10-02Univs: fixed bug 2584, correct universe found for mutual inductive.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-29 04:50:25 +0000