| Commit message (Expand) | Author | Age |
... | |
* | | merging conflicts with the original "trunk__CLEANUP__Context__2" branch | Matej Kosik | 2016-02-15 |
|\ \ |
|
* | | | Monotonizing the Evarutil module. | Pierre-Marie Pédrot | 2016-02-15 |
| * | | CLEANUP: Context.{Rel,Named}.Declaration.t | Matej Kosik | 2016-02-09 |
|/ / |
|
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-01-21 |
|\| |
|
| * | Update copyright headers. | Maxime Dénès | 2016-01-20 |
* | | CLEANUP: in the Reductionops module | Matej Kosik | 2015-12-17 |
* | | Making Evarutil.new_evar monotonous. | Pierre-Marie Pédrot | 2015-10-18 |
* | | Hardening the API of evarmaps. | Pierre-Marie Pédrot | 2015-09-26 |
| * | 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-08-02 |
|/ |
|
* | 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-07-16 |
* | Some dead code. | Hugo Herbelin | 2015-04-21 |
* | Fix bug #3532, providing universe inconsistency information when a | Matthieu Sozeau | 2015-03-04 |
* | Making unification of LetIn's expressions more consistent (see #3920). | Hugo Herbelin | 2015-01-19 |
* | Update headers. | Maxime Dénès | 2015-01-12 |
* | Reverting the tentative try to restore the use of second-order | Hugo Herbelin | 2015-01-07 |
* | 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-06 |
* | Tentatively trying to restore the use of second-order typed-based | Hugo Herbelin | 2015-01-03 |
* | An optimization in the use of unification candidates so as to get the | Hugo Herbelin | 2015-01-01 |
* | Simplifying second_order_matching: no need to invert the linear | Hugo Herbelin | 2014-12-30 |
* | Documenting check_record + changing a possibly undefined int into int option. | Hugo Herbelin | 2014-12-15 |
* | Two fixes in unification (bugs #3782 and #3709) | Matthieu Sozeau | 2014-12-12 |
* | Fine-tuning unification error (using OccurCheck in evarconv). | Hugo Herbelin | 2014-12-11 |
* | Setup hook to change the unification algorithm used by evarconv, | Matthieu Sozeau | 2014-12-09 |
* | Being consistent in making arbitrary choices in recursive calls to | Hugo Herbelin | 2014-12-02 |
* | Option -type-in-type continued (deactivate test for inferred sort of | Hugo Herbelin | 2014-11-19 |
* | 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-15 |
* | English typo in a function name of evarconv. | Hugo Herbelin | 2014-10-13 |
* | Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name | Matthieu Sozeau | 2014-10-11 |
* | Do not expand primitive projections eagerly in evarconv, but only | Matthieu Sozeau | 2014-10-10 |
* | Fixing the anomaly in bug #3045 (a filter was not type-safe in | Hugo Herbelin | 2014-10-08 |
* | 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-10-02 |
* | Simplify evarconv thanks to new delta status of projections, | Matthieu Sozeau | 2014-09-30 |
* | In evarconv and unification, expand folded primitive projections to | Matthieu Sozeau | 2014-09-29 |
* | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau | 2014-09-27 |
* | Fix canonical structure resolution which was launched on the results of | Matthieu Sozeau | 2014-09-26 |
* | Rename eq_constr functions in Evd to not break backward compatibility | Matthieu Sozeau | 2014-09-24 |
* | Move the specific map_constr_with_binders_left_to_right | Matthieu Sozeau | 2014-09-19 |
* | Fix constrMatching as well as change/e_contextually to allow | Matthieu Sozeau | 2014-09-18 |
* | 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-17 |