Monomorphized a lot of equalities over OCaml integers, thanks to

the new Int module. Only the most obvious were removed, so there
are a lot more in the wild.

This may sound heavyweight, but it has two advantages:

1. Monomorphization is explicit, hence we do not miss particular
optimizations of equality when doing it carelessly with the generic
equality.

2. When we have removed all the generic equalities on integers, we
will be able to write something like "let (=) = ()" to retrieve all
its other uses (mostly faulty) spread throughout the code, statically.

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

1 files changed, 3 insertions, 3 deletions

diff --git a/tactics/dn.ml b/tactics/dn.ml
index a0889ab8f..ea19ecc41 100644
--- a/tactics/dn.ml
+++ b/tactics/dn.ml
@@ -16,7 +16,7 @@ struct
 	  None,None -> 0
 	| Some (l,n),Some (l',n') -> 
 	    let m = Y.compare l l' in
-	    if m = 0 then
+	    if Int.equal m 0 then
 	      n-n' 
 	    else m
 	| Some(l,n),None -> 1
@@ -26,7 +26,7 @@ struct
     type t = X.t * Z.t
     let compare (x1,x2) (y1,y2) = 
       let m = (X.compare x1 y1) in
-      if m = 0 then (Z.compare x2 y2) else 
+      if Int.equal m 0 then (Z.compare x2 y2) else 
 	m
   end
 
@@ -65,7 +65,7 @@ prefix ordering, [dna] is the function returning the main node of a pattern *)
     try [T.map tm lbl, true] with Not_found -> []
       
   let rec skip_arg n tm =
-    if n = 0 then [tm,true]
+    if Int.equal n 0 then [tm,true]
     else
       List.flatten 
 	(List.map