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, 10 insertions, 9 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 25ea991e7b..ebda3cb76f 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -321,7 +321,7 @@ let split_product na' = function
   | _ -> anomaly "ill-formed fixpoint body"
 
 let rec split_fix n typ def =
-  if n = 0 then ([],typ,def)
+  if Int.equal n 0 then ([],typ,def)
   else
     let (na,_,def) = split_lambda def in
     let (na,t,typ) = split_product na typ in
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 2ec66bb346..26e9f9eb5d 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -621,9 +621,10 @@ let pr_fix_tac (id,n,c) =
           ln nal)
       [] bll in
   let idarg,bll = set_nth_name names n bll in
-  let annot =
-    if List.length names = 1 then mt()
-    else spc() ++ str"{struct " ++ pr_id idarg ++ str"}" in
+  let annot = match names with
+  | [_] -> mt ()
+  | _ -> spc() ++ str"{struct " ++ pr_id idarg ++ str"}"
+  in
   hov 1 (str"(" ++ pr_id id ++
         prlist pr_binder_fix bll ++ annot ++ str" :" ++
         pr_lconstrarg ty ++ str")") in
@@ -973,7 +974,7 @@ in (pr_tac, pr_match_rule)
 
 let strip_prod_binders_glob_constr n (ty,_) =
   let rec strip_ty acc n ty =
-    if n=0 then (List.rev acc, (ty,None)) else
+    if Int.equal n 0 then (List.rev acc, (ty,None)) else
       match ty with
           Glob_term.GProd(loc,na,Explicit,a,b) ->
             strip_ty (([Loc.ghost,na],(a,None))::acc) (n-1) b
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 4765045499..721d9b6c8a 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -495,7 +495,7 @@ let rec pr_vernac = function
   | VernacUnfocused -> str"Unfocused"
   | VernacGoal c -> str"Goal" ++ pr_lconstrarg c
   | VernacAbort id -> str"Abort" ++ pr_opt pr_lident id
-  | VernacUndo i -> if i=1 then str"Undo" else str"Undo" ++ pr_intarg i
+  | VernacUndo i -> if Int.equal i 1 then str"Undo" else str"Undo" ++ pr_intarg i
   | VernacUndoTo i -> str"Undo" ++ spc() ++ str"To" ++ pr_intarg i
   | VernacBacktrack (i,j,k) ->
       str "Backtrack" ++  spc() ++ prlist_with_sep sep int [i;j;k]
@@ -523,7 +523,7 @@ let rec pr_vernac = function
   (* Resetting *)
   | VernacResetName id -> str"Reset" ++ spc() ++ pr_lident id
   | VernacResetInitial -> str"Reset Initial"
-  | VernacBack i -> if i=1 then str"Back" else str"Back" ++ pr_intarg i
+  | VernacBack i -> if Int.equal i 1 then str"Back" else str"Back" ++ pr_intarg i
   | VernacBackTo i -> str"BackTo" ++ pr_intarg i
 
   (* State management *)
@@ -634,9 +634,9 @@ let rec pr_vernac = function
       let pr_constructor_list b l = match l with
         | Constructors [] -> mt()
         | Constructors l ->
+            let fst_sep = match l with [_] -> "   " | _ -> " | " in
             pr_com_at (begin_of_inductive l) ++
-            fnl() ++
-            str (if List.length l = 1 then "   " else " | ") ++
+            fnl() ++ str fst_sep ++
             prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l
        | RecordDecl (c,fs) ->
 	    spc() ++