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

5 files changed, 36 insertions, 29 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 7b6be410b9..e7300fceaf 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -988,7 +988,7 @@ let adjust_predicate_from_tomatch tomatch (current,typ as ct) pb =
 
 let rec ungeneralize n ng body =
   match kind_of_term body with
-  | Lambda (_,_,c) when ng = 0 ->
+  | Lambda (_,_,c) when Int.equal ng 0 ->
       subst1 (mkRel n) c
   | Lambda (na,t,c) ->
       (* We traverse an inner generalization *)
@@ -1046,8 +1046,8 @@ let rec irrefutable env = function
   | PatCstr (_,cstr,args,_) ->
       let ind = inductive_of_constructor cstr in
       let (_,mip) = Inductive.lookup_mind_specif env ind in
-      let one_constr = Array.length mip.mind_user_lc = 1 in
-      one_constr & List.for_all (irrefutable env) args
+      let one_constr = Int.equal (Array.length mip.mind_user_lc) 1 in
+      one_constr && List.for_all (irrefutable env) args
 
 let first_clause_irrefutable env = function
   | eqn::mat -> List.for_all (irrefutable env) eqn.patterns
@@ -1419,7 +1419,7 @@ let push_binder d (k,env,subst) =
 
 let rec list_assoc_in_triple x = function
     [] -> raise Not_found
-  | (a,b,_)::l -> if compare a x = 0 then b else list_assoc_in_triple x l
+  | (a, b, _)::l -> if Int.equal a x then b else list_assoc_in_triple x l
 
 (* Let vijk and ti be a set of dependent terms and T a type, all
  * defined in some environment env. The vijk and ti are supposed to be
@@ -1682,7 +1682,7 @@ let prepare_predicate_from_arsign_tycon loc tomatchs arsign c =
       let signlen = List.length sign in
 	match kind_of_term tm with
 	  | Rel n when dependent tm c
-		&& signlen = 1 (* The term to match is not of a dependent type itself *) ->
+		&& Int.equal signlen 1 (* The term to match is not of a dependent type itself *) ->
 	      ((n, len) :: subst, len - signlen)
 	  | Rel n when signlen > 1 (* The term is of a dependent type,
 				      maybe some variable in its type appears in the tycon. *) ->
@@ -2162,7 +2162,7 @@ let build_dependent_signature env evars avoid tomatchs arsign =
       ([], 0, [], nar, []) tomatchs arsign
   in
   let arsign'' = List.rev arsign' in
-    assert(slift = 0); (* we must have folded over all elements of the arity signature *)
+    assert(Int.equal slift 0); (* we must have folded over all elements of the arity signature *)
     arsign'', allnames, nar, eqs, neqs, refls
 
 let context_of_arsign l =
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index b417dc1d48..405e089a68 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -69,7 +69,8 @@ let nfirsts_app_of_stack n s =
   let (args, _) = strip_app s in List.firstn n args
 let list_of_app_stack s =
   let (out,s') = strip_app s in
-  Option.init (s' = []) out
+  let init = match s' with [] -> true | _ -> false in
+  Option.init init out
 let array_of_app_stack s =
   Option.map Array.of_list (list_of_app_stack s)
 let rec zip = function
@@ -93,7 +94,7 @@ let rec stack_assign s p c = match s with
           | _ -> assert false)
   | _ -> s
 let rec stack_tail p s =
-  if p = 0 then s else
+  if Int.equal p 0 then s else
     match s with
       | Zapp args :: s ->
 	  let q = List.length args in
@@ -188,11 +189,11 @@ module RedFlags = (struct
   let fiota = 16
   let fzeta = 32
   let mkflags = List.fold_left (lor) 0
-  let red_beta f = f land fbeta <> 0
-  let red_delta f = f land fdelta <> 0
-  let red_eta f = f land feta <> 0
-  let red_iota f = f land fiota <> 0
-  let red_zeta f = f land fzeta <> 0
+  let red_beta f = not (Int.equal (f land fbeta) 0)
+  let red_delta f = not (Int.equal (f land fdelta) 0)
+  let red_eta f = not (Int.equal (f land feta) 0)
+  let red_iota f = not (Int.equal (f land fiota) 0)
+  let red_zeta f = not (Int.equal (f land fzeta) 0)
 end : RedFlagsSig)
 
 open RedFlags
@@ -319,7 +320,7 @@ let rec whd_state_gen flags ts env sigma =
                           match kind_of_term x' with
                             | Rel 1 when l' = empty_stack ->
 				let lc = Array.sub cl 0 (napp-1) in
-				let u = if napp=1 then f else appvect (f,lc) in
+				let u = if Int.equal napp 1 then f else appvect (f,lc) in
 				if noccurn 1 u then (pop u,empty_stack) else s
                             | _ -> s
 			else s
@@ -375,7 +376,7 @@ let local_whd_state_gen flags sigma =
                           match kind_of_term x' with
                             | Rel 1 when l' = empty_stack ->
 				let lc = Array.sub cl 0 (napp-1) in
-				let u = if napp=1 then f else appvect (f,lc) in
+				let u = if Int.equal napp 1 then f else appvect (f,lc) in
 				if noccurn 1 u then (pop u,empty_stack) else s
                             | _ -> s
 			else s
@@ -690,7 +691,9 @@ let plain_instance s c =
     | _ ->
 	map_constr_with_binders succ irec n u
   in
-  if s = [] then c else irec 0 c
+  match s with
+  | [] -> c
+  | _ -> irec 0 c
 
 (* [instance] is used for [res_pf]; the call to [local_strong whd_betaiota]
    has (unfortunately) different subtle side effects:
@@ -804,7 +807,7 @@ let splay_arity env sigma c =
 let sort_of_arity env sigma c = snd (splay_arity env sigma c)
 
 let splay_prod_n env sigma n =
-  let rec decrec env m ln c = if m = 0 then (ln,c) else
+  let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else
     match kind_of_term (whd_betadeltaiota env sigma c) with
       | Prod (n,a,c0) ->
 	  decrec (push_rel (n,None,a) env)
@@ -814,7 +817,7 @@ let splay_prod_n env sigma n =
   decrec env n empty_rel_context
 
 let splay_lam_n env sigma n =
-  let rec decrec env m ln c = if m = 0 then (ln,c) else
+  let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else
     match kind_of_term (whd_betadeltaiota env sigma c) with
       | Lambda (n,a,c0) ->
 	  decrec (push_rel (n,None,a) env)
@@ -941,7 +944,9 @@ let meta_instance sigma b =
     List.map
       (fun mv -> (mv,meta_value sigma mv)) (Metaset.elements b.freemetas)
   in
-  if c_sigma = [] then b.rebus else instance sigma c_sigma b.rebus
+  match c_sigma with
+  | [] -> b.rebus
+  | _ -> instance sigma c_sigma b.rebus
 
 let nf_meta sigma c = meta_instance sigma (mk_freelisted c)
 
@@ -981,7 +986,9 @@ let meta_reducible_instance evd b =
 	 with Not_found -> u)
     | _ -> map_constr irec u
   in
-  if fm = [] then (* nf_betaiota? *) b.rebus else irec b.rebus
+  match fm with
+  | [] -> (* nf_betaiota? *) b.rebus
+  | _ -> irec b.rebus
 
 
 let head_unfold_under_prod ts env _ c =
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 97ce40a77b..29d0fa05e7 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -959,7 +959,7 @@ let unfold env sigma name =
 let unfoldoccs env sigma (occs,name) c =
   let unfo nowhere_except_in locs =
     let (nbocc,uc) = substlin env name 1 (nowhere_except_in,locs) c in
-    if nbocc = 1 then
+    if Int.equal nbocc 1 then
       error ((string_of_evaluable_ref env name)^" does not occur.");
     let rest = List.filter (fun o -> o >= nbocc) locs in
     if rest <> [] then error_invalid_occurrence rest;
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 2585d44898..8369972284 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -221,7 +221,7 @@ let lookup_rel_id id sign =
     | []                     -> raise Not_found
     | (Anonymous, _, _) :: l -> lookrec (n + 1) l
     | (Name id', b, t) :: l  ->
-      if Names.id_ord id' id = 0 then (n, b, t) else lookrec (n + 1) l
+      if Int.equal (Names.id_ord id' id) 0 then (n, b, t) else lookrec (n + 1) l
   in
   lookrec 1 sign
 
@@ -258,7 +258,7 @@ let rec strip_head_cast c = match kind_of_term c with
       let rec collapse_rec f cl2 = match kind_of_term f with
 	| App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
 	| Cast (c,_,_) -> collapse_rec c cl2
-	| _ -> if Array.length cl2 = 0 then f else mkApp (f,cl2)
+	| _ -> if Int.equal (Array.length cl2) 0 then f else mkApp (f,cl2)
       in
       collapse_rec f cl
   | Cast (c,_,_) -> strip_head_cast c
@@ -342,7 +342,7 @@ let fold_rec_types g (lna,typarray,_) e =
 
 let map_left2 f a g b =
   let l = Array.length a in
-  if l = 0 then [||], [||] else begin
+  if Int.equal l 0 then [||], [||] else begin
     let r = Array.create l (f a.(0)) in
     let s = Array.create l (g b.(0)) in
     for i = 1 to l - 1 do
@@ -911,7 +911,7 @@ let eq_constr = constr_cmp Reduction.CONV
 let split_app c = match kind_of_term c with
     App(c,l) ->
       let len = Array.length l in
-      if len=0 then ([],c) else
+      if Int.equal len 0 then ([],c) else
 	let last = Array.get l (len-1) in
 	let prev = Array.sub l 0 (len-1) in
 	c::(Array.to_list prev), last
@@ -981,7 +981,7 @@ let rec eta_reduce_head c =
                  (match kind_of_term cl.(lastn) with
                     | Rel 1 ->
 			let c' =
-                          if lastn = 1 then f
+                          if Int.equal lastn 1 then f
 			  else mkApp (f, Array.sub cl 0 lastn)
 			in
 			if noccurn 1 c'
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 447ee8e3bb..856c5e1477 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -395,7 +395,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
                let tyN = get_type_of curenv sigma cN in
                check_compatibility curenv substn tyM tyN);
 	    (* Here we check that [cN] does not contain any local variables *)
-	    if nb = 0 then
+	    if Int.equal nb 0 then
               sigma,(k,cN,snd (extract_instance_status pb))::metasubst,evarsubst
             else if noccur_between 1 nb cN then
               (sigma,
@@ -409,7 +409,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
                let tyN = Typing.meta_type sigma k in
                check_compatibility curenv substn tyM tyN);
 	    (* Here we check that [cM] does not contain any local variables *)
-	    if nb = 0 then
+	    if Int.equal nb 0 then
               (sigma,(k,cM,fst (extract_instance_status pb))::metasubst,evarsubst)
 	    else if noccur_between 1 nb cM
 	    then
@@ -771,7 +771,7 @@ let merge_instances env sigma flags st1 st2 c1 c2 =
 
 let applyHead env evd n c  =
   let rec apprec n c cty evd =
-    if n = 0 then
+    if Int.equal n 0 then
       (evd, c)
     else
       match kind_of_term (whd_betadeltaiota env evd cty) with