aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/opened
AgeCommit message (Collapse)Author
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-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-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-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-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
2014-06-17Not a bug, keep for backwards compatibilityMatthieu Sozeau
2014-06-17Bug closed, now in polymorphic mode, Variables A B : Type give different ↵Matthieu Sozeau
levels to A and B.
2014-06-17Explicit universes allow to write liftings explicitely. Implicit lifting ↵Matthieu Sozeau
would change the theory non-trivially.
2014-06-17Not considering test-suite file #89 as a bug anymore.Matthieu Sozeau
2014-06-17Continue fix on argument scopes of primitive projections.Matthieu Sozeau
2014-06-17Fix HoTT bug #84, binding scopes to projections.Matthieu Sozeau
2014-06-17HoTT coq bug #82 already fixed.Matthieu Sozeau
2014-06-17Adapt coercion code to work with projections as target classes.Matthieu Sozeau
2014-06-17- Fix the de Bruijn problem in check_projection for good :)Matthieu Sozeau
- Fix HoTT coq bug #80, implicit arguments with primitive projections were wrongly automatically infered.
2014-06-17Fix a de Bruijn bug in checking code of projections.Matthieu Sozeau
2014-06-17Existing Class now works with universe polymorphism. Fixes HoTT bug #063Matthieu Sozeau
2014-06-16Unification in HoTT_coq_061.v was looping with previous commit (whileHugo Herbelin
it was failing with Not_found before previous commit). This "fixes" the loop by expanding local defs in "imitate" rather than keeping them explicit. The example is otherwise too large for me to be able to understand where does the loop come from.
2014-06-16- Add "Show Universes" to print information about universes during a proof.Matthieu Sozeau
- Remove dead code in evarconv.
2014-06-16HoTT bug #29 is fixed, using the correct notion of polymorphic product types.Matthieu Sozeau
2014-06-15Change Ltac constr matching semantics to consider universes when merging twoMatthieu Sozeau
bindings of the same variable (fixing HoTT bug #52). Document the unification of universes in Ltac/tactics.
2014-06-15The semantics of Variable x y : T is to have the exact same type T for x and y,Matthieu Sozeau
while Context gives different type to each variable, this test-suite file shows this.
2014-06-15Remove HoTT bug #33, as the stdlib won't become polymorphic in the next version.Matthieu Sozeau
2014-06-15- Fix xml plugin treatment of inductives.Matthieu Sozeau
- Move HoTT bug #30 to closed
2014-06-13Fix HoTT/coq bug # 14. Now coercion code correctly raises an error instead ↵Matthieu Sozeau
of an anomaly in case a universe inconsistency occurs when applying a coercion. The statement of the test-suite file cannot check as is, but does check when the correct FunctorCategory is given, instantiating the TypeCat to Set.
2014-06-13HoTT/coq bug #7 is closed, and the definitions can be made to go through ↵Matthieu Sozeau
using explicit universes. The behavior of Hint Rewrite still differs from Hint Resolve though.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 03:18:45 +0000