aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Collapse)Author
2014-08-03Fixing #3483 (graceful failing with notations to non-constructors in "match").Hugo Herbelin
2014-07-31Finish fixes on notations and primitive projections, add test-suite files ↵Matthieu Sozeau
for closed bugs
2014-07-30Add test-suite file for bug #3439.Matthieu Sozeau
2014-07-29Add test-suite file for bug 3454.Matthieu Sozeau
2014-07-29Add test-suite file for bug #3453Matthieu Sozeau
2014-07-21Adding a test-suite for bug #3422.Pierre-Marie Pédrot
2014-07-16Adding a test-suite for bug #3416.Pierre-Marie Pédrot
2014-07-03Fix eta expansion of primitive records (HoTT bug #78), which now fails ↵Matthieu Sozeau
cleanly when called on partially applied constructors. Also protect evar_conv from that case.
2014-07-02Indeed simpl never is really honored now.Matthieu Sozeau
2014-06-30Tests for bugs #2834 and #2994.Hugo Herbelin
2014-06-30Completing test for bug report #2830Hugo Herbelin
2014-06-28Quickly fixing bug #2996: typing functions now check when referring toHugo Herbelin
a global reference that the current (goal) env contains all the section variables that the global reference expects to be present. Note that the test for inclusion might be costly: everytime a conversion happens in a section variable copied in a goal, this conversion has to be redone when referring to a constant dependent on this section variable. It is unclear to me whether we should not instead give global names to section variables so that they exist even if they are not listed in the context of the current goal. Here are two examples which are still problematic: Section A. Let B := True : Type. Definition C := eq_refl : B = True. Theorem D : Type. clearbody B. set (x := C). unfold C in x. (* inconsistent context *) or Section A. Let B : Type. exact True. Qed. Definition C := eq_refl : B = True. (* Note that this violated the Qed. *) Theorem D : Type. set (x := C). unfold C in x. (* inconsistent context *)
2014-06-26Invalid bug report.Matthieu Sozeau
2014-06-26Fix bug # 3325 using canonical structure declarations where needed.Matthieu Sozeau
2014-06-26Add an option to disable typeclass resolution during conversion, whichMatthieu Sozeau
is has non-local effects. For now it is not disabled by default, but we'll try to disable it once the test-suite and contribs are stabilized.
2014-06-26Merge branch 'tc-test-suite' of https://github.com/JasonGross/coq into ↵Matthieu Sozeau
JasonGross-tc
2014-06-26Fixed bug with new semantics of change.Matthieu Sozeau
2014-06-26DuplicateMatthieu Sozeau
2014-06-26This has been fixed.Matthieu Sozeau
2014-06-26Properly refresh the local hintdb database in case an external tactic changedMatthieu Sozeau
the hypotheses in eauto.
2014-06-26Fix test-suite file, adding the proper Fail.Matthieu Sozeau
2014-06-26Bug #3329 is closed.Matthieu Sozeau
2014-06-263392 is now closed thanks to E. Tassi.Matthieu Sozeau
2014-06-26Merge branch 'more-test-suite' of https://github.com/JasonGross/coq into ↵Matthieu Sozeau
JasonGross-more-test-suite Conflicts: test-suite/bugs/closed/3300.v test-suite/bugs/closed/3373.v
2014-06-26Fix test-suite files.Matthieu Sozeau
2014-06-26Bug #3301 is closed, the projection cannot be defined anymore.Matthieu Sozeau
2014-06-26Fix test-suite file for opened bug #1596Matthieu Sozeau
2014-06-26Fix test-suite file for bug # 3036, the unification has _never_ succeeded,Matthieu Sozeau
as this would result in an ill-scoped substitution.
2014-06-26Change interface of refresh universes to get a pbty argument instead ofMatthieu Sozeau
the computed direction argument. In case pbty is conv, no refreshing is done as the evar body must be convertible with the given term, however refreshing of template application evar arguments can still happen. (Re)-Closing bug #2966.
2014-06-26Add an Unset Standard...Matthieu Sozeau
2014-06-24Update some bugs about typeclass resolutionJason Gross
2014-06-23Fix handling of side effects in Defined objects (Closes: HoTT#111 + 3344)Enrico Tassi
Every time you use abstract a kitten dies, please stop.
2014-06-23Fix for bug 1951, allowing at least fully-applied inductives types to be usedMatthieu Sozeau
for building polymorphic instances of template polymorphic inductives.
2014-06-23Fix semantics of change p with c to typecheck c at each specific occurrence ↵Matthieu Sozeau
of p, avoiding unwanted universe constraints in presence of universe polymorphic constants. Fixing HoTT bugs # 36, 54 and 113.
2014-06-23Proper handling of the polymorphism flag for Context, fixing HoTT bug #98.Matthieu Sozeau
2014-06-23The uses of the funext axiom forced levels to Set, relaxing its use doesn't.Matthieu Sozeau
2014-06-23The test-suite file couldn't typecheck as it rightly introduces a universe ↵Matthieu Sozeau
inconsistency. One needs to use a universe level lower than eq's parameter for this to be consistent.
2014-06-23Fix test-suite script for HoTT coq bug #34Matthieu Sozeau
2014-06-22More test-suite casesJason Gross
2014-06-21- Add an option to refresh only algebraic universes, for e_type_of. The goalMatthieu Sozeau
there is not the same as in Evd.define. - Fixed bugs #3330 and #3331.
2014-06-20Fixed bug 3332.Matthieu Sozeau
2014-06-20Allow more relaxed conversion between the types of the two terms of a rewriteMatthieu Sozeau
equation, fix uncaught exception in setoid_rewrite (bug #3336).
2014-06-20Add fixed test-suite file for 3373.Matthieu Sozeau
2014-06-20Fix computation of inductive level in monomorphism + indices-matter mode.Matthieu Sozeau
Fixes bug #3346.
2014-06-20Fixed some HoTT bugs, provide a proper error message when giving an ill-formedMatthieu Sozeau
universe instance.
2014-06-20Bug 27 closed now that universe contexts can be refined during the proof,Matthieu Sozeau
here instantiating a flexible level with Set.
2014-06-19HoTT coq bug #62 fixed.Matthieu Sozeau
2014-06-18Proofs now take and return an evar_universe_context, simplifying interfacesMatthieu Sozeau
and avoiding explicit substitutions and merging of contexts, e.g. in obligations.ml. The context produced by typechecking a statement is passed in the proof, allowing the universe name context to be correctly folded as well. Mainly an API cleanup.
2014-06-17Fix a destArity that does not exactly match isArity in presence of let-ins.Matthieu Sozeau
2014-06-17Reinstate eta for records in evarconv, fixing two HoTT coq bugs.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 10:38:10 +0000