summaryrefslogtreecommitdiff
path: root/utils/diffing.mli
Commit message (Collapse)AuthorAgeFilesLines
* Tweaks to the documentationJules Aguillon2022-01-281-2/+1
|
* odoc: Fix syntax errors in commentsJules Aguillon2022-01-281-1/+1
|
* TyposJPR2021-08-261-2/+2
|
* Functorized diffing (with improved documentation) (#4)Florian Angeletti2021-06-221-53/+72
|
* swaps and movesFlorian Angeletti2021-06-221-2/+12
|
* diffing: define few common functionsFlorian Angeletti2021-06-221-0/+7
|
* Semantic diffings for functor types and applications (#9331)Gabriel Radanne2021-04-071-0/+112
This commit improves the error messages for ill-typed functor applications and inclusion between functor types. It does so by computing a diff between the expected and the provided types, and find an application that minimizes the error. The set of changes also paves the way for better diff for inclusion checks between signatures. * Implement a generic and variadic Wagner–Fischer algorithm for computing locally optimal paths. * Compute a full error tree for module type inclusion and equality errors * Improve the error message for module type equality * Expand the error message at the module level by using a diffing algorithm to analyze erroneous functor multi-applications or inclusions using Levenshtein distance. Co-authored-by: Florian Angeletti <florian.angeletti@inria.fr> Co-authored-by: octachron <octa@polychoron.fr>