aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.common
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-01-03 15:44:03 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-01-03 16:06:18 +0100
commit893a02f643858ba0b0172648e77af9ccb65f03df (patch)
treee5b835376bdf3e00e073608bdc18346513059973 /Makefile.common
parent353b523c0c808d0650cd77821363b0c865aedecf (diff)
Tentatively trying to restore the use of second-order typed-based
unification algorithm in consider_remaining_unif_problems. If it happens to be problematic, one can backtrack to the "optimization" from 3bd9cb26b which has a restriction on rels/vars.
Diffstat (limited to 'Makefile.common')
0 files changed, 0 insertions, 0 deletions