First debug... the renaming of librairies was not working and auto/dn were not taking in account equivalent names of inductive types.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12408 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 5 deletions

diff --git a/tactics/dn.ml b/tactics/dn.ml
index 8076e252c5..a0889ab8f4 100644
--- a/tactics/dn.ml
+++ b/tactics/dn.ml
@@ -15,15 +15,19 @@ struct
       match x,y with
 	  None,None -> 0
 	| Some (l,n),Some (l',n') -> 
-	    if (Y.compare l l') = 0 && n = n' then 0 
-	    else Pervasives.compare x y
-	| a,b -> Pervasives.compare a b 
+	    let m = Y.compare l l' in
+	    if m = 0 then
+	      n-n' 
+	    else m
+	| Some(l,n),None -> 1
+	| None, Some(l,n) -> -1
   end
   module X_tries = struct
     type t = X.t * Z.t
     let compare (x1,x2) (y1,y2) = 
-	    if (X.compare x1 y1) = 0 && (Z.compare x2 y2)=0 then 0 
-	    else Pervasives.compare (x1,x2) (y1,y2)
+      let m = (X.compare x1 y1) in
+      if m = 0 then (Z.compare x2 y2) else 
+	m
   end
 
   module T = Tries.Make(X_tries)(Y_tries)