aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
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-18Fixing #4198 (continued): not matching within the inner lambdas/let-insHugo Herbelin
of the return clause and of the branches (what assumed that the implementation preserves the invariant that the return predicate and the branches are in canonical [fun Δ => t] form, with Δ possibly containing let-ins).
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-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-13Fix some typos.Guillaume Melquiond
2015-10-12Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-11Adding test for bug #4366.Pierre-Marie Pédrot
2015-10-11Fixing test-suiteHugo Herbelin
2015-10-11Fixing untimely unexpected warning "Collision between bound variables" (#4317).Hugo Herbelin
Collecting the bound variables is now done on the glob_constr, before interpretation, so that only variables given explicitly by the user are used for binding bound variables.
2015-10-11Refining 0c320e79ba30 in fixing interpretation of constr under bindersHugo Herbelin
which was broken after it became possible to have binding names themselves bound to ltac variables (2fcc458af16b). Interpretation was corrected, but error message was damaged.
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-08Proof using: let-in policy, optional auto-clear, forward closure*Enrico Tassi
- "Proof using p*" means: use p and any section var about p. - Simplify the grammar/parser for proof using <expression>. - Section variables with a body (let-in) are pulled in automatically since they are safe to be used (add no extra quantification) - automatic clear of "unused" section variables made optional: Set Proof Using Clear Unused. since clearing section hypotheses does not "always work" (e.g. hint databases are not really cleaned) - term_typing: trigger a "suggest proof using" message also for Let theorems.
2015-10-07Fix bug #4069: f_equal regression.Matthieu Sozeau
2015-10-07Test for record syntax parsing.Pierre-Marie Pédrot
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: the stdlib now needs 5 universesMatthieu Sozeau
Prop < Set < i for every global univ i
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-02Fix test-suite fileMatthieu 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-25Updating the documentation and the toolchain w.r.t. the change in -compile.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-16In pat/constr introduction patterns, fixing in a better way clearing problemsHugo Herbelin
of temporary hypotheses than 76f27140e6e34 did.
2015-09-15Test for bug #4269.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 16:24:54 +0000