Implements the GDiff algorithm with a more realistic memory consumption,
and adapted to the generics-mrsop library. The original implementation of
gdiff carries around a number of unecessary proof objects, which makes it
unusable in real-life-sized diffs. The gdiff algorithm is described in this paper
We also provide a merge algorithm based on this repo,
for the stdiff approach. Read this paper
and/or this thesis for more information.