aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarconv.ml
Commit message (Expand)AuthorAge
* CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | CLEANUP: in the Reductionops moduleGravatar Matej Kosik2015-12-17
* | Making Evarutil.new_evar monotonous.Gravatar Pierre-Marie Pédrot2015-10-18
* | Hardening the API of evarmaps.Gravatar Pierre-Marie Pédrot2015-09-26
| * Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
| * Cosmetic changes in evarconv.ml: hopefully more regular names and formGravatar Hugo Herbelin2015-08-02
| * Cosmetic changes in evarconv.ml: hopefully more regular form andGravatar Hugo Herbelin2015-08-02
| * Cosmetic changes in evarconv.ml: hopefully using better self-documenting names.Gravatar Hugo Herbelin2015-08-02
| * Evarconv.ml: small cut-elimination, saving useless zip.Gravatar Hugo Herbelin2015-08-02
| * Cosmetic in evarconv.ml: naming a local function for better readibility.Gravatar Hugo Herbelin2015-08-02
|/
* Continuing 93579407, spotting other potential sources of anomalyGravatar Hugo Herbelin2015-07-16
* Fixing anomaly #3743 while printing an error message involving evar constraints.Gravatar Hugo Herbelin2015-07-16
* Some dead code.Gravatar Hugo Herbelin2015-04-21
* Fix bug #3532, providing universe inconsistency information when aGravatar Matthieu Sozeau2015-03-04
* Making unification of LetIn's expressions more consistent (see #3920).Gravatar Hugo Herbelin2015-01-19
* Update headers.Gravatar Maxime Dénès2015-01-12
* Reverting the tentative try to restore the use of second-orderGravatar Hugo Herbelin2015-01-07
* Propagating the relaxing of filtering started in 48509b6, fixed inGravatar Hugo Herbelin2015-01-06
* Fixing old filter bug in second_order_matching.Gravatar Hugo Herbelin2015-01-06
* Tentatively trying to restore the use of second-order typed-basedGravatar Hugo Herbelin2015-01-03
* An optimization in the use of unification candidates so as to get theGravatar Hugo Herbelin2015-01-01
* Simplifying second_order_matching: no need to invert the linearGravatar Hugo Herbelin2014-12-30
* Documenting check_record + changing a possibly undefined int into int option.Gravatar Hugo Herbelin2014-12-15
* Two fixes in unification (bugs #3782 and #3709)Gravatar Matthieu Sozeau2014-12-12
* Fine-tuning unification error (using OccurCheck in evarconv).Gravatar Hugo Herbelin2014-12-11
* Setup hook to change the unification algorithm used by evarconv,Gravatar Matthieu Sozeau2014-12-09
* Being consistent in making arbitrary choices in recursive calls toGravatar Hugo Herbelin2014-12-02
* Option -type-in-type continued (deactivate test for inferred sort ofGravatar Hugo Herbelin2014-11-19
* Reenable FO unification of primitive projections and their eta-expandedGravatar Matthieu Sozeau2014-10-15
* Modify the heuristic for unfolding lhs or rhs in evarconv, consideringGravatar Matthieu Sozeau2014-10-15
* English typo in a function name of evarconv.Gravatar Hugo Herbelin2014-10-13
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Do not expand primitive projections eagerly in evarconv, but onlyGravatar Matthieu Sozeau2014-10-10
* Fixing the anomaly in bug #3045 (a filter was not type-safe inGravatar Hugo Herbelin2014-10-08
* Work around issues with FO unification trying to unify terms ofGravatar Matthieu Sozeau2014-10-02
* Fix treatment of projections in Cst_stacks and unfolding behavior in evarconv.Gravatar Matthieu Sozeau2014-10-02
* Simplify evarconv thanks to new delta status of projections,Gravatar Matthieu Sozeau2014-09-30
* In evarconv and unification, expand folded primitive projections toGravatar Matthieu Sozeau2014-09-29
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Fix canonical structure resolution which was launched on the results ofGravatar Matthieu Sozeau2014-09-26
* Rename eq_constr functions in Evd to not break backward compatibilityGravatar Matthieu Sozeau2014-09-24
* Move the specific map_constr_with_binders_left_to_rightGravatar Matthieu Sozeau2014-09-19
* Fix constrMatching as well as change/e_contextually to allowGravatar Matthieu Sozeau2014-09-18
* Be more conservative and keep the use of eq_constr in pretyping/ functions.Gravatar Matthieu Sozeau2014-09-17
* Fix bug #3593, making constr_eq and progress work up toGravatar Matthieu Sozeau2014-09-17
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 16:44:13 +0000