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

6 files changed, 32 insertions, 28 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 97c954b8a..8daf11c70 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -77,7 +77,7 @@ type hint_entry = global_reference option * types gen_auto_tactic
 
 let pri_order_int (id1, {pri=pri1}) (id2, {pri=pri2}) =
   let d = pri1 - pri2 in
-    if d == 0 then id2 - id1
+    if Int.equal d 0 then id2 - id1
     else d
 
 let pri_order t1 t2 = pri_order_int t1 t2 <= 0
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index e8cde2967..819c76807 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -81,7 +81,7 @@ struct
       | _ -> Dn.Nothing
 
   let bounded_constr_pat_discr_st st (t,depth) =
-    if depth = 0 then 
+    if Int.equal depth 0 then 
       None 
     else
       match Term_dn.constr_pat_discr_st st t with
@@ -89,7 +89,7 @@ struct
 	| Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)
 	    
   let bounded_constr_val_discr_st st (t,depth) =
-    if depth = 0 then 
+    if Int.equal depth 0 then 
       Dn.Nothing 
     else
       match constr_val_discr_st st t with
@@ -98,7 +98,7 @@ struct
 	| Dn.Everything -> Dn.Everything
 
   let bounded_constr_pat_discr (t,depth) =
-    if depth = 0 then 
+    if Int.equal depth 0 then 
       None 
     else
       match Term_dn.constr_pat_discr t with
@@ -106,7 +106,7 @@ struct
 	| Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)
 	    
   let bounded_constr_val_discr (t,depth) =
-    if depth = 0 then 
+    if Int.equal depth 0 then 
       Dn.Nothing 
     else
       match constr_val_discr t with
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 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 9827b6146..63cdbfa92 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -296,14 +296,14 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c t l with_evars frze
     {elimindex = None; elimbody = (elim,NoBindings)} gl
 
 let adjust_rewriting_direction args lft2rgt =
-  if List.length args = 1 then begin
+  match args with
+  | [_] ->
     (* equality to a constant, like in eq_true *)
     (* more natural to see -> as the rewriting to the constant *)
     if not lft2rgt then
       error "Rewriting non-symmetric equality not allowed from right-to-left.";
     None
-  end
-  else
+  | _ ->
     (* other equality *)
     Some lft2rgt
 
@@ -931,7 +931,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
   let { intro = exist_term } = find_sigma_data sort_of_ty in
   let evdref = ref (Evd.create_goal_evar_defs sigma) in
   let rec sigrec_clausal_form siglen p_i =
-    if siglen = 0 then
+    if Int.equal siglen 0 then
       (* is the default value typable with the expected type *)
       let dflt_typ = type_of env sigma dflt in
       if Evarconv.e_cumul env evdref dflt_typ p_i then
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 69cee2148..20a52c21c 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -179,7 +179,7 @@ let fix_empty_or_and_pattern nv l =
 
 let check_or_and_pattern_size loc names n =
   if List.length names <> n then
-    if n = 1 then
+    if Int.equal n 1 then
       user_err_loc (loc,"",str "Expects a conjunctive pattern.")
     else
       user_err_loc (loc,"",str "Expects a disjunctive pattern with " ++ int n
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e55ba5d0e..39c669f42 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1211,7 +1211,7 @@ let keep hyps gl =
 (************************)
 
 let check_number_of_constructors expctdnumopt i nconstr =
-  if i=0 then error "The constructors are numbered starting from 1.";
+  if Int.equal i 0 then error "The constructors are numbered starting from 1.";
   begin match expctdnumopt with
     | Some n when n <> nconstr ->
 	error ("Not an inductive goal with "^
@@ -1243,7 +1243,7 @@ let any_constructor with_evars tacopt gl =
   let mind = fst (pf_reduce_to_quantified_ind gl (pf_concl gl)) in
   let nconstr =
     Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
-  if nconstr = 0 then error "The type has no constructors.";
+  if Int.equal nconstr 0 then error "The type has no constructors.";
   tclFIRST
     (List.map
       (fun i -> tclTHEN (constructor_tac with_evars None i NoBindings) t)
@@ -1286,9 +1286,9 @@ let error_unexpected_extra_pattern loc nb pat =
   | IntroIdentifier _ -> "name", (plural nb " introduction pattern"), "no"
   | _ -> "introduction pattern", "", "none" in
   user_err_loc (loc,"",str "Unexpected " ++ str s1 ++ str " (" ++
-    (if nb = 0 then (str s3 ++ str s2) else
+    (if Int.equal nb 0 then (str s3 ++ str s2) else
       (str "at most " ++ int nb ++ str s2)) ++ spc () ++
-       str (if nb = 1 then "was" else "were") ++
+       str (if Int.equal nb 1 then "was" else "were") ++
       strbrk " expected in the branch).")
 
 let intro_or_and_pattern loc b ll l' tac id gl =
@@ -1297,9 +1297,9 @@ let intro_or_and_pattern loc b ll l' tac id gl =
     let nv = mis_constr_nargs ind in
     let bracketed = b or not (l'=[]) in
     let rec adjust_names_length nb n = function
-      | [] when n = 0 or not bracketed -> []
+      | [] when Int.equal n 0 or not bracketed -> []
       | [] -> (dloc,IntroAnonymous) :: adjust_names_length nb (n-1) []
-      | (loc',pat) :: _ as l when n = 0 ->
+      | (loc',pat) :: _ as l when Int.equal n 0 ->
 	  if bracketed then error_unexpected_extra_pattern loc' nb pat;
 	  l
       | ip :: l -> ip :: adjust_names_length nb (n-1) l in
@@ -2239,7 +2239,7 @@ let empty_scheme =
   }
 
 let make_base n id =
-  if n=0 or n=1 then id
+  if Int.equal n 0 || Int.equal n 1 then id
   else
     (* This extends the name to accept new digits if it already ends with *)
     (* digits *)
@@ -2260,7 +2260,7 @@ let make_up_names n ind_opt cname =
     else add_prefix ind_prefix cname in
   let hyprecname = make_base n base_ind in
   let avoid =
-    if n=1 (* Only one recursive argument *) or n=0 then []
+    if Int.equal n 1 (* Only one recursive argument *) or Int.equal n 0 then []
     else
       (* Forbid to use cname, cname0, hyprecname and hyprecname0 *)
       (* in order to get names such as f1, f2, ... *)
@@ -2618,13 +2618,15 @@ let decompose_paramspred_branch_args elimt =
      type (See for example Empty_set_ind, as False would actually be ok). Then
      we must find the predicate of the conclusion to separate params_pred from
      args. We suppose there is only one predicate here. *)
-  if List.length acc2 <> 0 then acc1, acc2 , acc3, ccl
-  else
+  match acc2 with
+  | [] ->
     let hyps,ccl = decompose_prod_assum elimt in
     let hd_ccl_pred,_ = decompose_app ccl in
-    match kind_of_term hd_ccl_pred with
+    begin match kind_of_term hd_ccl_pred with
       | Rel i  -> let acc3,acc1 = cut_list (i-1) hyps in acc1 , [] , acc3 , ccl
       | _ -> error_ind_scheme ""
+    end
+  | _ -> acc1, acc2 , acc3, ccl
 
 
 let exchange_hd_app subst_hd t =
@@ -2694,7 +2696,7 @@ let compute_elim_sig ?elimc elimt =
       raise Exit
     end;
     (* 2- If no args_indargs (=!res.nargs at this point) then no indarg *)
-    if !res.nargs=0 then raise Exit;
+    if Int.equal !res.nargs 0 then raise Exit;
     (* 3- Look at last arg: is it the indarg? *)
     ignore (
       match List.hd args_indargs with
@@ -3166,7 +3168,7 @@ let new_induct_gen_l isrec with_evars elim (eqname,names) lc gl =
    args *)
 let induct_destruct isrec with_evars (lc,elim,names,cls) gl =
   assert (List.length lc > 0); (* ensured by syntax, but if called inside caml? *)
-  if List.length lc = 1 && not (is_functional_induction elim gl) then
+  if Int.equal (List.length lc) 1 && not (is_functional_induction elim gl) then
     (* standard induction *)
     onOpenInductionArg
       (fun c -> new_induct_gen isrec with_evars elim names c cls)
@@ -3182,7 +3184,8 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) gl =
       error "'in' clause not supported here.";
     let lc = List.map
       (map_induction_arg (pf_apply finish_evar_resolution gl)) lc in
-    if List.length lc = 1 then
+    begin match lc with
+    | [_] ->
       (* Hook to recover standard induction on non-standard induction schemes *)
       (* will be removable when is_functional_induction will be more clever *)
       onInductionArg
@@ -3190,7 +3193,7 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) gl =
 	  if lbind <> NoBindings then
 	    error "'with' clause not supported here.";
 	  new_induct_gen_l isrec with_evars elim names [c]) (List.hd lc) gl
-    else
+    | _ ->
       let newlc =
 	List.map (fun x ->
 	  match x with (* FIXME: should we deal with ElimOnIdent? *)
@@ -3198,6 +3201,7 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) gl =
 	  | _ -> error "Don't know where to find some argument.")
 	  lc in
       new_induct_gen_l isrec with_evars elim names newlc gl
+    end
   end
 
 let induction_destruct isrec with_evars = function