| Age | Commit message (Expand) | Author |
|---|
| 2015-01-06 | Propagating the relaxing of filtering started in 48509b6, fixed in | Hugo Herbelin |
| 2015-01-06 | Fixing old filter bug in second_order_matching. | Hugo Herbelin |
| 2015-01-03 | Tentatively trying to restore the use of second-order typed-based | Hugo Herbelin |
| 2015-01-01 | An optimization in the use of unification candidates so as to get the | Hugo Herbelin |
| 2014-12-30 | Simplifying second_order_matching: no need to invert the linear | Hugo Herbelin |
| 2014-12-15 | Documenting check_record + changing a possibly undefined int into int option. | Hugo Herbelin |
| 2014-12-12 | Two fixes in unification (bugs #3782 and #3709) | Matthieu Sozeau |
| 2014-12-11 | Fine-tuning unification error (using OccurCheck in evarconv). | Hugo Herbelin |
| 2014-12-09 | Setup hook to change the unification algorithm used by evarconv, | Matthieu Sozeau |
| 2014-12-02 | Being consistent in making arbitrary choices in recursive calls to | Hugo Herbelin |
| 2014-11-19 | Option -type-in-type continued (deactivate test for inferred sort of | Hugo Herbelin |
| 2014-10-15 | Reenable FO unification of primitive projections and their eta-expanded | Matthieu Sozeau |
| 2014-10-15 | Modify the heuristic for unfolding lhs or rhs in evarconv, considering | Matthieu Sozeau |
| 2014-10-13 | English typo in a function name of evarconv. | Hugo Herbelin |
| 2014-10-11 | Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name | Matthieu Sozeau |
| 2014-10-10 | Do not expand primitive projections eagerly in evarconv, but only | Matthieu Sozeau |
| 2014-10-08 | Fixing the anomaly in bug #3045 (a filter was not type-safe in | Hugo Herbelin |
| 2014-10-02 | Work around issues with FO unification trying to unify terms of | Matthieu Sozeau |
| 2014-10-02 | Fix treatment of projections in Cst_stacks and unfolding behavior in evarconv. | Matthieu Sozeau |
| 2014-09-30 | Simplify evarconv thanks to new delta status of projections, | Matthieu Sozeau |
| 2014-09-29 | In evarconv and unification, expand folded primitive projections to | Matthieu Sozeau |
| 2014-09-27 | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau |
| 2014-09-26 | Fix canonical structure resolution which was launched on the results of | Matthieu Sozeau |
| 2014-09-24 | Rename eq_constr functions in Evd to not break backward compatibility | Matthieu Sozeau |
| 2014-09-19 | Move the specific map_constr_with_binders_left_to_right | Matthieu Sozeau |
| 2014-09-18 | Fix constrMatching as well as change/e_contextually to allow | Matthieu Sozeau |
| 2014-09-17 | Be more conservative and keep the use of eq_constr in pretyping/ functions. | Matthieu Sozeau |
| 2014-09-17 | Fix bug #3593, making constr_eq and progress work up to | Matthieu Sozeau |
| 2014-09-17 | Revert specific syntax for primitive projections, avoiding ugly | Matthieu Sozeau |
| 2014-09-13 | Providing a -type-in-type option for collapsing the universe hierarchy. | Hugo Herbelin |
| 2014-09-12 | Uniformisation of the order of arguments env and sigma. | Hugo Herbelin |
| 2014-09-11 | Fix bug #3594: eta for constructors and functions at the same time which | Matthieu Sozeau |
| 2014-09-08 | Fix bug #3589, unification looping due to incorrect use of stack with primiti... | Matthieu Sozeau |
| 2014-09-04 | Print [Variant] types with the keyword [Variant]. | Arnaud Spiwack |
| 2014-09-01 | In evarconv, do first-order unification of LetIn's properly, ensuring we comp... | Matthieu Sozeau |
| 2014-08-28 | Change the way primitive projections are declared to the kernel. | Matthieu Sozeau |
| 2014-08-28 | There are some occurs-check cases that can be handled by imitation (using pru... | Matthieu Sozeau |
| 2014-08-26 | Make evarconv and unification able to handle eta for records in presence | Matthieu Sozeau |
| 2014-08-25 | Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible | Matthieu Sozeau |
| 2014-08-14 | Restrict eta-conversion to inductive records, fixing bug #3310. | Matthieu Sozeau |
| 2014-08-10 | Fix bug introduced by earlier commit on first-order unification of primitive | Matthieu Sozeau |
| 2014-08-09 | Fix unification which was failing when unifying a primitive projection against | Matthieu Sozeau |
| 2014-08-08 | Fix evarconv not applying eta when it used to. Fixes bug#3319. | Matthieu Sozeau |
| 2014-07-09 | Revert patch making the oracle be used for the transparent state in evarconv, | Matthieu Sozeau |
| 2014-07-07 | In flex-flex cases, the undefinedness of an evar can not be preseved after co... | Matthieu Sozeau |
| 2014-07-03 | Fix eta expansion of primitive records (HoTT bug #78), which now fails cleanl... | Matthieu Sozeau |
| 2014-06-25 | Use full transparent state when checking well-typedness of a second order mat... | Matthieu Sozeau |
| 2014-06-17 | Reinstate eta for records in evarconv, fixing two HoTT coq bugs. | Matthieu Sozeau |
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot |
| 2014-06-16 | - Add "Show Universes" to print information about universes during a proof. | Matthieu Sozeau |
