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

3 files changed, 8 insertions, 8 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index d5f96e3fd6..b651053dba 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -274,7 +274,7 @@ let drop_implicits_in_patt cst nb_expl args =
 	|None -> aux t
 	|x -> x
      in
-     if nb_expl = 0 then aux impl_data
+     if Int.equal nb_expl 0 then aux impl_data
      else
        let imps = List.skipn_at_least nb_expl (select_stronger_impargs impl_st) in
        impls_fit [] (imps,args)
@@ -712,7 +712,7 @@ let rec extern inctx scopes vars r =
 		 let projs = struc.Recordops.s_PROJ in
 		 let locals = struc.Recordops.s_PROJKIND in
 		 let rec cut args n =
-		   if n = 0 then args
+		   if Int.equal n 0 then args
 		   else
 		     match args with
 		     | [] -> raise No_match
@@ -907,7 +907,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
                   subscopes,impls
                 | _ ->
                   [], [] in
-	      (if n = 0 then f else GApp (Loc.ghost,f,args1)),
+	      (if Int.equal n 0 then f else GApp (Loc.ghost,f,args1)),
 	      args2, subscopes, impls
 	  | GApp (_,(GRef (_,ref) as f),args), None ->
 	      let subscopes = find_arguments_scope ref in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c204db0e01..a6b207c1da 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -199,7 +199,7 @@ and spaces ntn n =
 
 let expand_notation_string ntn n =
   let pos = List.nth (wildcards ntn 0) n in
-  let hd = if pos = 0 then "" else String.sub ntn 0 pos in
+  let hd = if Int.equal pos 0 then "" else String.sub ntn 0 pos in
   let tl =
     if pos = String.length ntn then ""
     else String.sub ntn (pos+1) (String.length ntn - pos -1) in
@@ -737,7 +737,7 @@ let find_remaining_scopes pl1 pl2 ref =
   let impls_st = implicits_of_global ref in
   let len_pl1 = List.length pl1 in
   let len_pl2 = List.length pl2 in
-  let impl_list = if len_pl1 = 0
+  let impl_list = if Int.equal len_pl1 0
     then select_impargs_size len_pl2 impls_st
     else List.skipn_at_least len_pl1 (select_stronger_impargs impls_st) in
   let allscs = find_arguments_scope ref in
@@ -797,7 +797,7 @@ let check_constructor_length env loc cstr len_pl pl0 =
         (nargs - (Inductiveops.inductive_nparams (fst cstr))))
 
 let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 =
-  let impl_list = if len_pl1 = 0
+  let impl_list = if Int.equal len_pl1 0
     then select_impargs_size (List.length pl2) impls_st
     else List.skipn_at_least len_pl1 (select_stronger_impargs impls_st) in
   let remaining_args = List.fold_left (fun i x -> if is_status_implicit x then i else succ i) in
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index c5cc1438b8..d3c55c1f58 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -754,7 +754,7 @@ let rec match_cases_pattern metas sigma a1 a2 =
       when r1 = r2 ->
       let l1 = add_patterns_for_params (fst r1) args1 in
       let le2 = List.length l2 in
-      if le2 = 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1
+      if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1
       then
 	raise No_match
       else
@@ -777,7 +777,7 @@ let match_ind_pattern metas sigma ind pats a2 =
   | NApp (NRef (IndRef r2),l2)
       when ind = r2 ->
       let le2 = List.length l2 in
-      if le2 = 0 (* Special case of a notation for a @Cstr *) || le2 > List.length pats
+      if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length pats
       then
 	raise No_match
       else