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, 19 insertions, 15 deletions

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