| Age | Commit message (Expand) | Author |
|---|
| 2016-02-19 | Fixing bug #4580: [Set Refine Instance Mode] also used for Program Instance. | Pierre-Marie Pédrot |
| 2016-02-19 | Fixing bug #4582: cannot override notation [ x ]. | Pierre-Marie Pédrot |
| 2016-02-17 | Fix bug #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity"). | Pierre-Marie Pédrot |
| 2016-02-13 | Do not give a name to anonymous evars anymore. See bug #4547. | Pierre-Marie Pédrot |
| 2016-01-24 | Adding a test for bug #4378. | Pierre-Marie Pédrot |
| 2016-01-24 | Fixing bug #4495: Failed assertion in metasyntax.ml. | Pierre-Marie Pédrot |
| 2016-01-24 | Fixing bug #4511: evar tactic can create non-typed evars. | Pierre-Marie Pédrot |
| 2016-01-23 | Fix bug #4503: mixing universe polymorphic and monomorphic | Matthieu Sozeau |
| 2016-01-23 | Fix bug #4519: oops, global shadowed local universe level bindings. | Matthieu Sozeau |
| 2016-01-19 | Fix bug #4420: check_types was losing universe constraints. | Matthieu Sozeau |
| 2016-01-13 | Fixing success of test for #3848 after move to directory "closed". | Hugo Herbelin |
| 2016-01-12 | Fixing #4467 (missing shadowing of variables in cases pattern). | Hugo Herbelin |
| 2016-01-12 | Fixing #4256 and #4484 (changes in evar-evar resolution made that new | Hugo Herbelin |
| 2016-01-07 | Fix bug #4480: progress was not checked for setoid_rewrite. | Matthieu Sozeau |
| 2015-12-31 | Put implicits back as in 8.4. | Matthieu Sozeau |
| 2015-12-31 | Fix bug #4456, anomaly in handle-side effects | Matthieu Sozeau |
| 2015-12-29 | Fixing bug #4462: unshelve: Anomaly: Uncaught exception Not_found. | Pierre-Marie Pédrot |
| 2015-12-22 | Inclusion of functors with restricted signature is now forbidden (fix #3746) | Pierre Letouzey |
| 2015-12-17 | (Partial) fix for bug #4453: raise an error instead of an anomaly. | Matthieu Sozeau |
| 2015-12-15 | Extraction: more cautious use of intermediate result caching (fix #3923) | Pierre Letouzey |
| 2015-12-15 | Fix test-suite files after change in refine tactic. | Maxime Dénès |
| 2015-12-15 | Refine tactic now shelves unifiable holes. | Pierre-Marie Pédrot |
| 2015-12-14 | Test file for #4363 was not complete. | Maxime Dénès |
| 2015-12-11 | Univs: Fix bug #4363, nested abstract. | Matthieu Sozeau |
| 2015-12-03 | Univs: fix bug #4443. | Matthieu Sozeau |
| 2015-12-02 | Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG. | Hugo Herbelin |
| 2015-11-30 | Test for bug #4149. | Pierre-Marie Pédrot |
| 2015-11-28 | Test-suite files for closed bugs | Matthieu Sozeau |
| 2015-11-28 | Closed bugs. | Matthieu Sozeau |
| 2015-11-27 | Univs: entirely disallow instantiation of polymorphic constants with | Matthieu Sozeau |
| 2015-11-19 | Fix bug #4429: eauto with arith: 70x performance regression in Coq 8.5. | Pierre-Marie Pédrot |
| 2015-11-12 | Fix bug #4412: [rewrite] (setoid_rewrite?) creates ill-typed terms. | Pierre-Marie Pédrot |
| 2015-11-12 | Fixed test-suite file for bug #3998. | Matthieu Sozeau |
| 2015-11-11 | Now closed. | Matthieu Sozeau |
| 2015-11-11 | Fix bug #3257, setoid_reflexivity should fail if not completing the goal. | Matthieu Sozeau |
| 2015-11-11 | Fix bug #4293: ensure let-ins do not contain algebraic universes in | Matthieu Sozeau |
| 2015-11-11 | Fixing bug #3554: Anomaly: Anonymous implicit argument. | Pierre-Marie Pédrot |
| 2015-11-10 | Test for bug #4404. | Pierre-Marie Pédrot |
| 2015-11-05 | Add test-suite file for #4273. | Matthieu Sozeau |
| 2015-11-04 | Univs: missing checks in evarsolve with candidates and missing a | Matthieu Sozeau |
| 2015-11-04 | Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusion | Matthieu Sozeau |
| 2015-11-04 | Test file for #4397. | Maxime Dénès |
| 2015-11-02 | Fix bug #4151: discrepancy between exact and eexact/eassumption. | Matthieu Sozeau |
| 2015-11-02 | Refresh rigid universes as well, and in 8.4 compatibility mode, | Matthieu Sozeau |
| 2015-10-29 | Fixing another instance of bug #3267 in eauto, this time in the | Hugo Herbelin |
| 2015-10-28 | Univs: fix bug #4375, accept universe binders on (co)-fixpoints | Matthieu Sozeau |
| 2015-10-27 | Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names | Matthieu Sozeau |
| 2015-10-26 | Two test-suite files for bugs 3974 and 3975 | Pierre Letouzey |
| 2015-10-24 | Backtracking on interpreting toplevel calls to exact in scope determined | Hugo Herbelin |
| 2015-10-21 | Bug #3956 is fixed. | Matthieu Sozeau |
