Removing a bunch of generic equalities.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 9 insertions, 9 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index d02711eeb3..a45fe179ae 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -137,7 +137,7 @@ let build_by_tactic env typ tac =
   let ce = build_constant_by_tactic id sign typ tac in
   let ce = Term_typing.handle_side_effects env ce in
   let cb, se = Future.force ce.const_entry_body in
-  assert(se = Declareops.no_seff);
+  assert(Declareops.side_effects_is_empty se);
   cb
 
 (**********************************************************************)
diff --git a/proofs/proof.ml b/proofs/proof.ml
index c1a909aedc..8ad2458afa 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -66,17 +66,17 @@ end
 let check_cond_kind c k =
   let kind_of_cond = function
     | CondNo (_,k) | CondDone(_,k) | CondEndStack k -> k in
-  kind_of_cond c = k
+  Int.equal (kind_of_cond c) k
 
 let test_cond c k1 pw =
   match c with
-  | CondNo(_,     k) when k = k1 -> Strict
+  | CondNo(_,     k) when Int.equal k k1 -> Strict
   | CondNo(true,  _)             -> Loose
   | CondNo(false, _)             -> Cannot NotThisWay
-  | CondDone(_,     k) when k = k1 && Proofview.finished pw -> Strict
+  | CondDone(_,     k) when Int.equal k k1 && Proofview.finished pw -> Strict
   | CondDone(true,  _)                                      -> Loose
   | CondDone(false, _)                                      -> Cannot NotThisWay
-  | CondEndStack k when k = k1 -> Strict
+  | CondEndStack k when Int.equal k k1 -> Strict
   | CondEndStack _             -> Cannot AlreadyNoFocus
 
 let no_cond ?(loose_end=false) k = CondNo (loose_end, k)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 2365e2bdbd..d773eeb43d 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -185,17 +185,17 @@ let check_no_pending_proof () =
   end
 
 let discard_gen id =
-  pstates := List.filter (fun { pid = id' } -> id <> id') !pstates
+  pstates := List.filter (fun { pid = id' } -> not (Id.equal id id')) !pstates
 
 let discard (loc,id) =
   let n = List.length !pstates in
   discard_gen id;
-  if List.length !pstates = n then
+  if Int.equal (List.length !pstates) n then
     Errors.user_err_loc
       (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs ())
 
 let discard_current () =
-  if !pstates = [] then raise NoCurrentProof else pstates := List.tl !pstates
+  if List.is_empty !pstates then raise NoCurrentProof else pstates := List.tl !pstates
 
 let discard_all () = pstates := []
 
@@ -249,7 +249,7 @@ let set_used_variables l =
   match !pstates with
   | [] -> raise NoCurrentProof
   | p :: rest ->
-      if p.section_vars <> None then
+      if not (Option.is_empty p.section_vars) then
         Errors.error "Used section variables can be declared only once";
       pstates := { p with section_vars = Some ctx} :: rest