aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
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-29Handle side-effects of Vernacular commands inside proofs better, so thatMatthieu Sozeau
universes are declared correctly in the enclosing proofs evar_map's.
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-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-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-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-21Removing test for bug #3956.Pierre-Marie Pédrot
It breaks test-suite of trunk since Matthieu's fixes for the soundness of polymorphic universes, and I am unsure of the expected semantics. We should reintroduce it later on when we understand better the issue of simply fix it once and for all.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 12:55:45 +0000