aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2015-10-28Fix test suite after Matthieu's ed7af646f2e486b.Maxime Dénès
2015-10-28test cases.Gregory Malecha
2015-10-28Univs: fix bug #4375, accept universe binders on (co)-fixpointsMatthieu Sozeau
2015-10-28Revert "Fixing #4198 (continued): not matching within the inner lambdas/let-ins"Hugo Herbelin
After all, let's target 8.6.
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-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-22Fixing a bug in reporting ill-formed inductive.Hugo Herbelin
Was introduced in b06d3badb (15 Jul 2015).
2015-10-21Bug #3956 is fixed.Matthieu Sozeau
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-15Test file for #4346: Set is no longer of type TypeMaxime Dénès
2015-10-13Fix some typos.Guillaume Melquiond
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-09Refine fix for handling of the universe contexts of hints, depending onMatthieu Sozeau
their polymorphic status _and_ locality.
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-06Fix bug #4354: interpret hints in the right env and sigma.Matthieu Sozeau
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-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-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
2015-09-15STM: Reset takes Ltac <ident> into account (Close #4316)Enrico Tassi
2015-09-08Fixing incomplete bugfix in 76f27140e6e34 (unfortunately 5 commitsHugo Herbelin
ago) which broke compilation of theories/Logic/WKL.v (collision between a temporary name and a user name).
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-17 16:25:33 +0000