aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Collapse)Author
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
2015-10-02Univs: fix Universe vernacular, fix bug #4287.Matthieu Sozeau
No universe can be set lower than Prop anymore (or Set).
2015-10-02Univs: fixed bug #4328.Matthieu Sozeau
2015-10-02Forcing i > Set for global universes (incomplete)Matthieu Sozeau
2015-09-26Test for bug #4347.Pierre-Marie Pédrot
2015-09-25Merge branch 'v8.5'Pierre-Marie Pédrot
2015-09-20Test file for #3948 - Anomaly: unknown constant in Print Assumptions.Maxime Dénès
2015-09-17Merge branch 'v8.5' into trunkMaxime Dénès
2015-09-15STM: Reset takes Ltac <ident> into account (Close #4316)Enrico Tassi
2015-08-22Merge branch 'v8.5'Pierre-Marie Pédrot
2015-08-21Fixing #4318 (anomaly when applying args to a recursive notation in patterns).Hugo Herbelin
I don't know what was the intent of Pierre B here. In 8.4, it was not supported, raising with an error at parsing time. I changed the anomaly into an error at interpretation time, so it is still not supported but we could support it if some legitimate use of it eventually appears.
2015-08-14Move type_scope into user space, fix some output logsJason Gross
2015-08-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-08-03Test file for #4254: Mutual inductives with parameters on Type raises anomaly.Maxime Dénès
2015-08-02Fixing #4221 (interpreting bound variables using ltac env was possiblyHugo Herbelin
capturing bound names unexpectingly). We moved renaming to after finding bindings, i.e. in pretyping "fun x y => x + y" in an ltac environment where y is ltac-bound to x, we type the body in environment "x y |-" but build "fun y y => Rel 2 + Rel 1" (which later on is displayed into "fun y y0 => y + y0"). We renounced to renaming in "match" patterns, which was anyway not working well, as e.g. in let x := ipattern:y in (forall z, match z with S x => x | x => x end = 0). which was producing forall z : nat, match z with 0 => z | S y => y end = 0 because the names in default branches are treated specifically. It would be easy to support renaming in match again, by putting the ltac env in the Cases.pattern_matching_problem state and to rename the names in "typs" (from build_branch), just before returning them at the end of the function (and similarly in abstract_predicate for the names occurring in the return predicate). However, we rename binders in fix which were not interpreted. There are some difficulties with evar because we want them defined in the interpreted env (see comment to ltac_interp_name_env). fix ltac name
2015-07-29Adding test for bug #3779.Pierre-Marie Pédrot
2015-07-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-28Adding a test for bug #4280.Pierre-Marie Pédrot
2015-07-28Updating test-suite for #3510.Pierre-Marie Pédrot
2015-07-28Tests for bugs #3509 and #3510.Pierre-Marie Pédrot
2015-07-27Test for bug #2243.Pierre-Marie Pédrot
2015-07-27Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-27Fixing #4305 (compatibility wrt 8.4 in not interpreting anHugo Herbelin
abbreviation not bound to an applied constructor as itself but rather as a binding variable as it was the case for non-applied constructor). This was broken by e5c02503 while fixed #3483 (Not_found uncaught with a notation to a non-constructor).
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-30 15:14:57 +0000