From 86e2b0ab9da7dbd9c4c39ab2ab8df05d94a42056 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 28 Jul 2015 13:42:30 +0200
Subject: 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.
---
 tactics/term_dnet.ml | 4 ++--
 1 file 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
 
-- 
cgit v1.2.3