| Age | Commit message (Expand) | Author |
|---|
| 2016-03-16 | Fix incorrect behavior of CS resolution | Matthieu Sozeau |
| 2016-03-10 | Primitive projections: protect kernel from erroneous definitions. | Matthieu Sozeau |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2015-08-02 | Reverting 16 last commits, committed mistakenly using the wrong push command. | Hugo Herbelin |
| 2015-08-02 | Cosmetic changes in evarconv.ml: hopefully more regular names and form | Hugo Herbelin |
| 2015-08-02 | Cosmetic changes in evarconv.ml: hopefully more regular form and | Hugo Herbelin |
| 2015-08-02 | Cosmetic changes in evarconv.ml: hopefully using better self-documenting names. | Hugo Herbelin |
| 2015-08-02 | Evarconv.ml: small cut-elimination, saving useless zip. | Hugo Herbelin |
| 2015-08-02 | Cosmetic in evarconv.ml: naming a local function for better readibility. | Hugo Herbelin |
| 2015-07-16 | Continuing 93579407, spotting other potential sources of anomaly | Hugo Herbelin |
| 2015-07-16 | Fixing anomaly #3743 while printing an error message involving evar constraints. | Hugo Herbelin |
| 2015-04-21 | Some dead code. | Hugo Herbelin |
| 2015-03-04 | Fix bug #3532, providing universe inconsistency information when a | Matthieu Sozeau |
| 2015-01-19 | Making unification of LetIn's expressions more consistent (see #3920). | Hugo Herbelin |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2015-01-07 | Reverting the tentative try to restore the use of second-order | Hugo Herbelin |
| 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 |
