| Age | Commit message (Expand) | Author |
|---|
| 2015-11-26 | Fixing the "parsing rules with idents later declared as keywords" problem. | Hugo Herbelin |
| 2015-11-22 | Fixing a vm_compute bug in the presence of let-ins among the | Hugo Herbelin |
| 2015-11-22 | Fixing a bug of adjust_subst_to_rel_context. | Hugo Herbelin |
| 2015-11-22 | Fixing kernel bug in typing match with let-ins in the arity. | Hugo Herbelin |
| 2015-11-19 | Fix bug #4429: eauto with arith: 70x performance regression in Coq 8.5. | Pierre-Marie Pédrot |
| 2015-11-18 | Fixing logical bugs in the presence of let-ins in computiong primitive | Hugo Herbelin |
| 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-07 | Fixing output test Existentials.v after eec77191b. | Hugo Herbelin |
| 2015-11-07 | Tests for syntax "Show id" and [id]:tac (shelved or not). | Hugo Herbelin |
| 2015-11-06 | Fixing complexity file f_equal.v. | Hugo Herbelin |
| 2015-11-06 | Fixing complexity issue with f_equal. Thanks to J.-H. Jourdan | Hugo Herbelin |
| 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 | Hint Cut documentation and cleanup of printing (was duplicated and | 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 | Handle side-effects of Vernacular commands inside proofs better, so that | Matthieu Sozeau |
| 2015-10-29 | Fixing another instance of bug #3267 in eauto, this time in the | Hugo Herbelin |
| 2015-10-28 | Fix test suite after Matthieu's ed7af646f2e486b. | Maxime Dénès |
| 2015-10-28 | test cases. | Gregory Malecha |
| 2015-10-28 | Univs: fix bug #4375, accept universe binders on (co)-fixpoints | Matthieu Sozeau |
| 2015-10-28 | Revert "Fixing #4198 (continued): not matching within the inner lambdas/let-ins" | Hugo Herbelin |
| 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-22 | Fixing a bug in reporting ill-formed inductive. | Hugo Herbelin |
| 2015-10-21 | Bug #3956 is fixed. | Matthieu Sozeau |
| 2015-10-19 | Test for #4372 (anomaly in inversion in the presence of fake dependency). | Hugo Herbelin |
| 2015-10-18 | Fixing #4198 (continued): not matching within the inner lambdas/let-ins | Hugo Herbelin |
| 2015-10-17 | Test for bug #4325. | Pierre-Marie Pédrot |
| 2015-10-15 | Test file for #4346: Set is no longer of type Type | Maxime Dénès |
| 2015-10-13 | Fix some typos. | Guillaume Melquiond |
| 2015-10-11 | Adding test for bug #4366. | Pierre-Marie Pédrot |
| 2015-10-11 | Fixing test-suite | Hugo Herbelin |
| 2015-10-11 | Fixing untimely unexpected warning "Collision between bound variables" (#4317). | Hugo Herbelin |
| 2015-10-11 | Refining 0c320e79ba30 in fixing interpretation of constr under binders | Hugo Herbelin |
| 2015-10-09 | Refine fix for handling of the universe contexts of hints, depending on | Matthieu Sozeau |
| 2015-10-08 | Univs: fix bug #4161. | Matthieu Sozeau |
| 2015-10-08 | Proof using: let-in policy, optional auto-clear, forward closure* | Enrico Tassi |
| 2015-10-07 | Fix bug #4069: f_equal regression. | Matthieu Sozeau |
| 2015-10-07 | Test for record syntax parsing. | Pierre-Marie Pédrot |
| 2015-10-07 | Univs: add Strict Universe Declaration option (on by default) | Matthieu Sozeau |
