diff options
| author | Hugo Herbelin | 2016-03-28 06:25:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-09 15:38:49 +0200 |
| commit | 92aea31430f9d0e8a0fc8f0d6b7fd1a221768f6c (patch) | |
| tree | 34ac00f915cc64c87be3e93d3d7c57bb7afea85c /kernel | |
| parent | 1cdb96f0201b4dda6bdb5f326f60314ae9bf700b (diff) | |
Reverting dbdff037 which does not seem to prevent to have #3638 fixed
on the contrary of message given in 23041481f, while it introduces a
square time complexity of the size of the goal in subterm finding.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions