diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-01-03 15:44:03 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-01-03 16:06:18 +0100 |
commit | 893a02f643858ba0b0172648e77af9ccb65f03df (patch) | |
tree | e5b835376bdf3e00e073608bdc18346513059973 /proofs/tacmach.ml | |
parent | 353b523c0c808d0650cd77821363b0c865aedecf (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 'proofs/tacmach.ml')
0 files changed, 0 insertions, 0 deletions