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 | |
| 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.
| -rw-r--r-- | tactics/term_dnet.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index e79fc6dc9a..65239a5f70 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -98,8 +98,8 @@ struct | DSort, DSort -> 0 | DRef gr1, DRef gr2 -> RefOrdered.compare gr1 gr2 | DCtx (tl1, tr1), DCtx (tl2, tr2) - | DLambda (tl1, tr1), DCtx (tl2, tr2) - | DApp (tl1, tr1), DCtx (tl2, tr2) -> + | DLambda (tl1, tr1), DLambda (tl2, tr2) + | DApp (tl1, tr1), DApp (tl2, tr2) -> let c = cmp tl1 tl2 in if c = 0 then cmp tr1 tr2 else c |