diff options
| author | Pierre-Marie Pédrot | 2015-07-28 13:42:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-07-28 13:42:30 +0200 |
| commit | 86e2b0ab9da7dbd9c4c39ab2ab8df05d94a42056 (patch) | |
| tree | b41d61b5183de5f034b4133059a77ed4564a2160 /kernel/nativelambda.mli | |
| parent | 71b101172275a7c5872f6e8e70f9c0185f93f828 (diff) | |
Fixing bug #3509 and #3510 (anomalies in "tactics/term_dnet.ml").
Commit dc438047 was a bit overlooked as it introduced a wrong comparison function
on term patterns in dnets. Strangely enough, it seems not to have wreaked havoc
that much compared to the severity of the error.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions