aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/opened
Commit message (Expand)AuthorAge
* Fix test-suite files, and move some opened to closed.Gravatar Matthieu Sozeau2014-09-11
* Status error for bug #3459.Gravatar Pierre-Marie Pédrot2014-09-04
* Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleGravatar Matthieu Sozeau2014-08-25
* Fix test-suite file.Gravatar Matthieu Sozeau2014-08-18
* Restrict eta-conversion to inductive records, fixing bug #3310.Gravatar Matthieu Sozeau2014-08-14
* Fix evarconv not applying eta when it used to. Fixes bug#3319.Gravatar Matthieu Sozeau2014-08-08
* Fix eta expansion of primitive records (HoTT bug #78), which now fails cleanl...Gravatar Matthieu Sozeau2014-07-03
* Indeed simpl never is really honored now.Gravatar Matthieu Sozeau2014-07-02
* Invalid bug report.Gravatar Matthieu Sozeau2014-06-26
* Fix bug # 3325 using canonical structure declarations where needed.Gravatar Matthieu Sozeau2014-06-26
* Add an option to disable typeclass resolution during conversion, whichGravatar Matthieu Sozeau2014-06-26
* Merge branch 'tc-test-suite' of https://github.com/JasonGross/coq into JasonG...Gravatar Matthieu Sozeau2014-06-26
|\
* | Fixed bug with new semantics of change.Gravatar Matthieu Sozeau2014-06-26
* | DuplicateGravatar Matthieu Sozeau2014-06-26
* | This has been fixed.Gravatar Matthieu Sozeau2014-06-26
* | Properly refresh the local hintdb database in case an external tactic changedGravatar Matthieu Sozeau2014-06-26
* | Fix test-suite file, adding the proper Fail.Gravatar Matthieu Sozeau2014-06-26
* | Bug #3329 is closed.Gravatar Matthieu Sozeau2014-06-26
* | 3392 is now closed thanks to E. Tassi.Gravatar Matthieu Sozeau2014-06-26
* | Merge branch 'more-test-suite' of https://github.com/JasonGross/coq into Jaso...Gravatar Matthieu Sozeau2014-06-26
|\ \
* | | Fix test-suite files.Gravatar Matthieu Sozeau2014-06-26
* | | Bug #3301 is closed, the projection cannot be defined anymore.Gravatar Matthieu Sozeau2014-06-26
* | | Fix test-suite file for opened bug #1596Gravatar Matthieu Sozeau2014-06-26
| | * Update some bugs about typeclass resolutionGravatar Jason Gross2014-06-24
| |/ |/|
* | Fix handling of side effects in Defined objects (Closes: HoTT#111 + 3344)Gravatar Enrico Tassi2014-06-23
| * More test-suite casesGravatar Jason Gross2014-06-22
|/
* - Add an option to refresh only algebraic universes, for e_type_of. The goalGravatar Matthieu Sozeau2014-06-21
* Fixed bug 3332.Gravatar Matthieu Sozeau2014-06-20
* Allow more relaxed conversion between the types of the two terms of a rewriteGravatar Matthieu Sozeau2014-06-20
* Fix computation of inductive level in monomorphism + indices-matter mode.Gravatar Matthieu Sozeau2014-06-20
* Fixed some HoTT bugs, provide a proper error message when giving an ill-formedGravatar Matthieu Sozeau2014-06-20
* Bug 27 closed now that universe contexts can be refined during the proof,Gravatar Matthieu Sozeau2014-06-20
* HoTT coq bug #62 fixed.Gravatar Matthieu Sozeau2014-06-19
* Proofs now take and return an evar_universe_context, simplifying interfacesGravatar Matthieu Sozeau2014-06-18
* Fix a destArity that does not exactly match isArity in presence of let-ins.Gravatar Matthieu Sozeau2014-06-17
* Reinstate eta for records in evarconv, fixing two HoTT coq bugs.Gravatar Matthieu Sozeau2014-06-17
* Not a bug, keep for backwards compatibilityGravatar Matthieu Sozeau2014-06-17
* Bug closed, now in polymorphic mode, Variables A B : Type give different leve...Gravatar Matthieu Sozeau2014-06-17
* Explicit universes allow to write liftings explicitely. Implicit lifting woul...Gravatar Matthieu Sozeau2014-06-17
* Not considering test-suite file #89 as a bug anymore.Gravatar Matthieu Sozeau2014-06-17
* Continue fix on argument scopes of primitive projections.Gravatar Matthieu Sozeau2014-06-17
* Fix HoTT bug #84, binding scopes to projections.Gravatar Matthieu Sozeau2014-06-17
* HoTT coq bug #82 already fixed.Gravatar Matthieu Sozeau2014-06-17
* Adapt coercion code to work with projections as target classes.Gravatar Matthieu Sozeau2014-06-17
* - Fix the de Bruijn problem in check_projection for good :)Gravatar Matthieu Sozeau2014-06-17
* Fix a de Bruijn bug in checking code of projections.Gravatar Matthieu Sozeau2014-06-17
* Existing Class now works with universe polymorphism. Fixes HoTT bug #063Gravatar Matthieu Sozeau2014-06-17
* Unification in HoTT_coq_061.v was looping with previous commit (whileGravatar Hugo Herbelin2014-06-16
* - Add "Show Universes" to print information about universes during a proof.Gravatar Matthieu Sozeau2014-06-16
* HoTT bug #29 is fixed, using the correct notion of polymorphic product types.Gravatar Matthieu Sozeau2014-06-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 18:06:23 +0000