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

10 files changed, 29 insertions, 27 deletions

diff --git a/toplevel/backtrack.ml b/toplevel/backtrack.ml
index 2d919e966..4e4b2135d 100644
--- a/toplevel/backtrack.ml
+++ b/toplevel/backtrack.ml
@@ -146,7 +146,7 @@ let sync nb_opened_proofs =
     the end. *)
 
 let back count =
-  if count = 0 then 0
+  if Int.equal count 0 then 0
   else
     let nb_opened_proofs = List.length (Pfedit.get_all_proof_names ()) in
     npop count;
diff --git a/toplevel/class.ml b/toplevel/class.ml
index ff0e9fcfb..87310302c 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -242,7 +242,7 @@ let add_new_coercion_core coef stre source target isid =
   if coercion_exists coef then raise (CoercionError AlreadyExists);
   let tg,lp = prods_of t in
   let llp = List.length lp in
-  if llp = 0 then raise (CoercionError NotAFunction);
+  if Int.equal llp 0 then raise (CoercionError NotAFunction);
   let (cls,lvs,ind) =
     try
       get_source lp source
diff --git a/toplevel/command.ml b/toplevel/command.ml
index edde7c652..f707ea508 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -36,7 +36,7 @@ open Indschemes
 open Misctypes
 
 let rec under_binders env f n c =
-  if n = 0 then f env Evd.empty c else
+  if Int.equal n 0 then f env Evd.empty c else
     match kind_of_term c with
       | Lambda (x,t,c) ->
 	  mkLambda (x,t,under_binders (push_rel (x,None,t) env) f (n-1) c)
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index c0027ef03..b6d1f981c 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -312,7 +312,7 @@ let explain_ill_typed_rec_body env sigma i names vdefj vargs =
   let pvd,pvdt = pr_ljudge_env env (vdefj.(i)) in
   let pv = pr_lconstr_env env vargs.(i) in
   str "The " ++
-  (if Array.length vdefj = 1 then mt () else pr_nth (i+1) ++ spc ()) ++
+  (if Int.equal (Array.length vdefj) 1 then mt () else pr_nth (i+1) ++ spc ()) ++
   str "recursive definition" ++ spc () ++ pvd ++ spc () ++
   str "has type" ++ spc () ++ pvdt ++ spc () ++
   str "while it should be" ++ spc () ++ pv ++ str "."
@@ -809,7 +809,7 @@ let error_ill_formed_inductive env c v =
 
 let error_ill_formed_constructor env id c v nparams nargs =
   let pv = pr_lconstr_env env v in
-  let atomic = (nb_prod c = 0) in
+  let atomic = Int.equal (nb_prod c) 0 in
   str "The type of constructor" ++ brk(1,1) ++ pr_id id ++ brk(1,1) ++
   str "is not valid;" ++ brk(1,1) ++
   strbrk (if atomic then "it must be " else "its conclusion must be ") ++
@@ -917,8 +917,8 @@ let explain_bad_constructor env cstr ind =
   str "is expected."
 
 let decline_string n s =
-  if n = 0 then "no "^s^"s"
-  else if n = 1 then "1 "^s
+  if Int.equal n 0 then "no "^s^"s"
+  else if Int.equal n 1 then "1 "^s
   else (string_of_int n^" "^s^"s")
 
 let explain_wrong_numarg_constructor env cstr n =
@@ -1020,7 +1020,7 @@ let explain_ltac_call_trace (nrep,last,trace,loc) =
 		     pr_id id ++ str ":=" ++ Printer.pr_lconstr_under_binders c)
 		  (List.rev vars @ unboundvars) ++ str ")"
 	      else mt())) ++
-      (if n=2 then str " (repeated twice)"
+      (if Int.equal n 2 then str " (repeated twice)"
        else if n>2 then str " (repeated "++int n++str" times)"
        else mt()) in
     if calls <> [] then
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 747f5835f..a49305292 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -292,7 +292,7 @@ let start_proof_with_initialization kind recguard thms snl hook =
             else
               tacl)),guard
   | None ->
-      assert (List.length thms = 1);
+      let () = match thms with [_] -> () | _ -> assert false in
       (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in
   match thms with
   | [] -> anomaly "No proof to start"
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index ed6b45228..345147157 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -35,7 +35,7 @@ let cache_token (_,s) = Lexer.add_keyword s
 
 let inToken : string -> obj =
   declare_object {(default_object "TOKEN") with
-       open_function = (fun i o -> if i=1 then cache_token o);
+       open_function = (fun i o -> if Int.equal i 1 then cache_token o);
        cache_function = cache_token;
        subst_function = Libobject.ident_subst_function;
        classify_function = (fun o -> Substitute o)}
@@ -84,7 +84,7 @@ let classify_tactic_notation tacobj =
 
 let inTacticGrammar : tactic_grammar_obj -> obj =
   declare_object {(default_object "TacticGrammar") with
-       open_function = (fun i o -> if i=1 then cache_tactic_notation o);
+       open_function = (fun i o -> if Int.equal i 1 then cache_tactic_notation o);
        cache_function = cache_tactic_notation;
        subst_function = subst_tactic_notation;
        classify_function = classify_tactic_notation}
@@ -180,7 +180,7 @@ let parse_format ((loc, str) : lstring) =
     | cur::l -> (a::cur)::l
     | [] -> [[a]] in
   let push_white n l =
-    if n = 0 then l else push_token (UnpTerminal (String.make n ' ')) l in
+    if Int.equal n 0 then l else push_token (UnpTerminal (String.make n ' ')) l in
   let close_box i b = function
     | a::(_::_ as l) -> push_token (UnpBox (b,a)) l
     | _ -> error "Non terminated box in format." in
@@ -195,7 +195,7 @@ let parse_format ((loc, str) : lstring) =
     if i < String.length str & str.[i] <> ' ' then
       if str.[i] = '\'' & quoted &
         (i+1 >= String.length str or str.[i+1] = ' ')
-      then if n=0 then error "Empty quoted token." else n
+      then if Int.equal n 0 then error "Empty quoted token." else n
       else nonspaces quoted (n+1) (i+1)
     else
       if quoted then error "Spaces are not allowed in (quoted) symbols."
@@ -240,7 +240,7 @@ let parse_format ((loc, str) : lstring) =
 	  push_token (UnpTerminal (String.sub str (i-1) (n+2)))
 	    (parse_token (close_quotation (i+n))))
     else
-      if n = 0 then []
+      if Int.equal n 0 then []
       else error "Ending spaces non part of a format annotation."
   and parse_box box i =
     let n = spaces 0 i in
@@ -760,7 +760,7 @@ let classify_syntax_definition (local, _ as o) =
 
 let inSyntaxExtension : syntax_extension_obj -> obj =
   declare_object {(default_object "SYNTAX-EXTENSION") with
-       open_function = (fun i o -> if i = 1 then cache_syntax_extension o);
+       open_function = (fun i o -> if Int.equal i 1 then cache_syntax_extension o);
        cache_function = cache_syntax_extension;
        subst_function = subst_syntax_extension;
        classify_function = classify_syntax_definition}
@@ -1008,7 +1008,7 @@ let open_notation i (_, nobj) =
   let scope = nobj.notobj_scope in
   let (ntn, df) = nobj.notobj_notation in
   let pat = nobj.notobj_interp in
-  if i = 1 & not (Notation.exists_notation_in_scope scope ntn pat) then begin
+  if Int.equal i 1 && not (Notation.exists_notation_in_scope scope ntn pat) then begin
     (* Declare the interpretation *)
     Notation.declare_notation_interpretation ntn scope pat df;
     (* Declare the uninterpretation *)
@@ -1229,7 +1229,7 @@ let load_scope_command _ (_,(scope,dlm)) =
   Notation.declare_scope scope
 
 let open_scope_command i (_,(scope,o)) =
-  if i=1 then
+  if Int.equal i 1 then
     match o with
     | ScopeDelim dlm -> Notation.declare_delimiters scope dlm
     | ScopeClasses cl -> List.iter (Notation.declare_scope_class scope) cl
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 6277faf27..5210a3c9e 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -149,7 +149,7 @@ let trunc_named_context n ctx =
     List.firstn (len - n) ctx
 
 let rec chop_product n t =
-  if n = 0 then Some t
+  if Int.equal n 0 then Some t
   else
     match kind_of_term t with
       | Prod (_, _, b) ->  if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None
@@ -645,7 +645,7 @@ let get_prog_err n =
 let get_any_prog_err () =
   try get_any_prog () with NoObligations id -> pperror (explain_no_obligations id)
 
-let obligations_solved prg = (snd prg.prg_obligations) = 0
+let obligations_solved prg = Int.equal (snd prg.prg_obligations) 0
 
 let all_programs () =
   ProgMap.fold (fun k p l -> p :: l) !from_prg []
@@ -657,7 +657,7 @@ type progress =
 
 let obligations_message rem =
   if rem > 0 then
-    if rem = 1 then
+    if Int.equal rem 1 then
       Flags.if_verbose msg_info (int rem ++ str " obligation remaining")
     else
       Flags.if_verbose msg_info (int rem ++ str " obligations remaining")
@@ -898,7 +898,7 @@ let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic
   let info = str (string_of_id n) ++ str " has type-checked" in
   let prg = init_prog_info n term t [] None [] obls implicits kind reduce hook in
   let obls,_ = prg.prg_obligations in
-  if Array.length obls = 0 then (
+  if Int.equal (Array.length obls) 0 then (
     Flags.if_verbose msg_info (info ++ str ".");
     let cst = declare_definition prg in
       Defined cst)
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index ec390683f..175a95165 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -56,8 +56,8 @@ let emacs_prompt_endstring() = Printer.emacs_str "</prompt>"
    beginning of line. *)
 let prompt_char ic ibuf count =
   let bol = match ibuf.bols with
-    | ll::_ -> ibuf.len == ll
-    | [] -> ibuf.len == 0
+    | ll::_ -> Int.equal ibuf.len ll
+    | [] -> Int.equal ibuf.len 0
   in
   if bol && not !print_emacs then msgerr (str (ibuf.prompt()));
   try
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 7cff9a4ec..42b9411f8 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -170,7 +170,9 @@ let restore_timeout = function
 
 let open_utf8_file_in fname =
   let is_bom s =
-    Char.code s.[0] = 0xEF && Char.code s.[1] = 0xBB && Char.code s.[2] = 0xBF
+    Int.equal (Char.code s.[0]) 0xEF &&
+    Int.equal (Char.code s.[1]) 0xBB &&
+    Int.equal (Char.code s.[2]) 0xBF
   in
   let in_chan = open_in fname in
   let s = "   " in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 42c36f519..71f7f39a3 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -259,7 +259,7 @@ let print_namespace ns =
         begin match match_dirpath ns dir with
         | Some [] as y -> y
         | Some (a::ns') ->
-            if Names.id_ord a id = 0 then Some ns'
+            if Int.equal (Names.id_ord a id) 0 then Some ns'
             else None
         | None -> None
         end
@@ -272,7 +272,7 @@ let print_namespace ns =
         begin match match_modulepath ns mp with
         | Some [] as y -> y
         | Some (a::ns') ->
-            if Names.id_ord a id = 0 then Some ns'
+            if Int.equal (Names.id_ord a id) 0 then Some ns'
             else None
         | None -> None
         end
@@ -1551,7 +1551,7 @@ let vernac_undoto n =
 let vernac_focus gln =
   let p = Proof_global.give_me_the_proof () in
   let n = match gln with None -> 1 | Some n -> n in
-  if n = 0 then
+  if Int.equal n 0 then
     Errors.error "Invalid goal number: 0. Goal numbering starts with 1."
   else
     Proof.focus focus_command_cond () n p; print_subgoals ()