Monomorphization (proof)

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

13 files changed, 92 insertions, 63 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 0dbaccc33..ebb1cbcd4 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -150,7 +150,7 @@ let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
 
 let mentions clenv mv0 =
   let rec menrec mv1 =
-    mv0 = mv1 ||
+    Int.equal mv0 mv1 ||
     let mlist =
       try match meta_opt_fvalue clenv.evd mv1 with
       | Some (b,_) -> b.freemetas
@@ -445,7 +445,7 @@ let clenv_assign_binding clenv k c =
   { clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd }
 
 let clenv_match_args bl clenv =
-  if bl = [] then
+  if List.is_empty bl then
     clenv
   else
     let mvs = clenv_independent clenv in
@@ -473,17 +473,17 @@ let error_not_right_number_missing_arguments n =
       int n ++ str ").")
 
 let clenv_constrain_dep_args hyps_only bl clenv =
-  if bl = [] then
+  if List.is_empty bl then
     clenv
   else
     let occlist = clenv_dependent_gen hyps_only clenv in
-    if List.length occlist = List.length bl then
+    if Int.equal (List.length occlist) (List.length bl) then
       List.fold_left2 clenv_assign_binding clenv occlist bl
     else
       if hyps_only then
 	(* Tolerance for compatibility <= 8.3 *)
 	let occlist' = clenv_dependent_gen hyps_only ~iter:false clenv in
-	if List.length occlist' = List.length bl then
+	if Int.equal (List.length occlist') (List.length bl) then
 	  List.fold_left2 clenv_assign_binding clenv occlist' bl
 	else
 	  error_not_right_number_missing_arguments (List.length occlist)
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index ff13cd46a..2c1b9d21f 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -52,7 +52,7 @@ let clenv_value_cast_meta clenv =
 
 let clenv_pose_dependent_evars with_evars clenv =
   let dep_mvs = clenv_dependent clenv in
-  if dep_mvs <> [] & not with_evars then
+  if not (List.is_empty dep_mvs) && not with_evars then
     raise
       (RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
   clenv_pose_metas_as_evars clenv dep_mvs
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index fb8e6b16e..8f7513371 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -17,9 +17,9 @@ open Evarutil
 (******************************************)
 
 let depends_on_evar evk _ (pbty,_,t1,t2) =
-  try head_evar t1 = evk
+  try Int.equal (head_evar t1) evk
   with NoHeadEvar ->
-  try head_evar t2 = evk
+  try Int.equal (head_evar t2) evk
   with NoHeadEvar -> false
 
 let define_and_solve_constraints evk c evd =
diff --git a/proofs/goal.ml b/proofs/goal.ml
index b7be860b5..c076cd676 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open Pp
 open Term
 
@@ -180,8 +181,8 @@ module Refinable = struct
   let rec fusion l1 l2 = match l1 , l2 with
     | [] , _ -> l2
     | _ , [] -> l1
-    | a::l1 , b::_ when a>b -> a::(fusion l1 l2)
-    | a::l1 , b::l2 when a=b -> a::(fusion l1 l2)
+    | a::l1 , b::_ when a > b -> a::(fusion l1 l2)
+    | a::l1 , b::l2 when Int.equal a b -> a::(fusion l1 l2)
     | _ , b::l2 -> b::(fusion l1 l2)
 
   let update_handle handle init_defs post_defs =
@@ -353,7 +354,7 @@ let plus s1 s2 env rdefs goal info =
   with UndefinedHere -> s2 env rdefs goal info
 
 (* Equality of two goals *)
-let equal { content = e1 } { content = e2 } = e1 = e2
+let equal { content = e1 } { content = e2 } = Int.equal e1 e2
 
 let here goal value _ _ goal' _ =
   if equal goal goal' then
@@ -426,7 +427,7 @@ let rename_hyp_sign id1 id2 sign =
     (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d)
 let rename_hyp id1 id2 env rdefs gl info =
   let hyps = hyps env rdefs gl info in
-  if id1 <> id2 &&
+  if not (Names.id_eq id1 id2) &&
     List.mem id2 (Termops.ids_of_named_context (Environ.named_context_of_val hyps)) then
        Errors.error ((Names.string_of_id id2)^" is already used.");
   let new_hyps = rename_hyp_sign id1 id2 hyps in
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 5437d2ba1..725f16b8e 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -147,10 +147,10 @@ let find_q x (m,q) =
   let rec find accs acc = function
       [] -> raise Not_found
     | [(x',l)] ->
-        if x=x' then ((v,Idset.union accs l),(m',List.rev acc))
+        if id_eq x x' then ((v,Idset.union accs l),(m',List.rev acc))
         else raise Not_found
     | (x',l as i)::((x'',l'')::q as itl) ->
-        if x=x' then
+        if id_eq x x' then
           ((v,Idset.union accs l),
            (m',List.rev acc@(x'',Idset.add x (Idset.union l l''))::q))
         else find (Idset.union l accs) (i::acc) itl in
@@ -163,7 +163,7 @@ let occur_vars_in_decl env hyps d =
 
 let reorder_context env sign ord =
   let ords = List.fold_right Idset.add ord Idset.empty in
-  if List.length ord <> Idset.cardinal ords then
+  if not (Int.equal (List.length ord) (Idset.cardinal ords)) then
     error "Order list has duplicates";
   let rec step ord expected ctxt_head moved_hyps ctxt_tail =
     match ord with
@@ -211,10 +211,17 @@ let check_decl_position env sign (x,_,_ as d) =
  * on the right side [right] if [toleft=false].
  * If [with_dep] then dependent hypotheses are moved accordingly. *)
 
+let move_location_eq m1 m2 = match m1, m2 with
+| MoveAfter id1, MoveAfter id2 -> id_eq id1 id2
+| MoveBefore id1, MoveBefore id2 -> id_eq id1 id2
+| MoveLast, MoveLast -> true
+| MoveFirst, MoveFirst -> true
+| _ -> false
+
 let rec get_hyp_after h = function
   | [] -> error_no_such_hypothesis h
   | (hyp,_,_) :: right ->
-      if hyp = h then
+      if id_eq hyp h then
 	match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveFirst
       else
        get_hyp_after h right
@@ -223,11 +230,14 @@ let split_sign hfrom hto l =
   let rec splitrec left toleft = function
     | [] -> error_no_such_hypothesis hfrom
     | (hyp,c,typ) as d :: right ->
-      	if hyp = hfrom then
-	  (left,right,d, toleft or hto = MoveLast)
+      	if id_eq hyp hfrom then
+	  (left,right,d, toleft || move_location_eq hto MoveLast)
       	else
-	  splitrec (d::left)
-	    (toleft or hto = MoveAfter hyp or hto = MoveBefore hyp)
+          let is_toleft = match hto with
+          | MoveAfter h' | MoveBefore h' -> id_eq hyp h'
+          | _ -> false
+          in
+	  splitrec (d::left) (toleft || is_toleft)
 	    right
   in
     splitrec [] false l
@@ -249,12 +259,12 @@ let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
 	if match hto with MoveFirst | MoveLast -> false | _ -> true then
 	  error_no_such_hypothesis (hyp_of_move_location hto);
 	List.rev first @ List.rev middle
-    | (hyp,_,_) :: _ as right when hto = MoveBefore hyp ->
+    | (hyp,_,_) :: _ as right when move_location_eq hto (MoveBefore hyp) ->
 	List.rev first @ List.rev middle @ right
     | (hyp,_,_) as d :: right ->
 	let (first',middle') =
       	  if List.exists (test_dep d) middle then
-	    if with_dep & hto <> MoveAfter hyp then
+	    if with_dep && not (move_location_eq hto (MoveAfter hyp)) then
 	      (first, d::middle)
             else
 	      errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id idfrom ++
@@ -264,7 +274,7 @@ let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
           else
 	    (d::first, middle)
 	in
-      	if hto = MoveAfter hyp then
+      	if move_location_eq hto (MoveAfter hyp) then
 	  List.rev first' @ List.rev middle' @ right
       	else
 	  moverec first' middle' right
@@ -340,7 +350,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	(** we keep the casts (in particular VMcast) except
 	    when they are annotating metas *)
 	if isMeta t then begin
-	  assert (k <> VMcast);
+	  assert (k != VMcast);
 	  res
 	end else
 	  let (gls,cty,sigma,trm) = res in
@@ -526,7 +536,7 @@ let prim_refiner r sigma goal =
      	let rec check_ind env k cl =
           match kind_of_term (strip_outer_cast cl) with
             | Prod (na,c1,b) ->
-            	if k = 1 then
+            	if Int.equal k 1 then
 		  try
 		    fst (find_inductive env sigma c1)
 		  with Not_found ->
@@ -541,7 +551,7 @@ let prim_refiner r sigma goal =
      	let rec mk_sign sign = function
 	  | (f,n,ar)::oth ->
 	      let (sp',_)  = check_ind env n ar in
-	      if not (sp=sp') then
+	      if not (eq_mind sp sp') then
 		error ("Fixpoints should be on the same " ^
 		       "mutual inductive declaration.");
 	      if !check && mem_named_context f (named_context_of_val sign) then
@@ -622,7 +632,7 @@ let prim_refiner r sigma goal =
 	check_typability env sigma cl';
 	if (not !check) || is_conv_leq env sigma cl' cl then
           let (sg,ev,sigma) = mk_goal sign cl' in
-	  let ev = if k<>DEFAULTcast then mkCast(ev,k,cl) else ev in
+	  let ev = if k != DEFAULTcast then mkCast(ev,k,cl) else ev in
 	  let sigma = Goal.V82.partial_solution sigma goal ev in
           ([sg], sigma)
 	else
@@ -669,7 +679,7 @@ let prim_refiner r sigma goal =
         ([gl], sigma)
 
     | Rename (id1,id2) ->
-        if !check & id1 <> id2 &&
+        if !check && not (id_eq id1 id2) &&
 	  List.mem id2 (ids_of_named_context (named_context_of_val sign)) then
           error ((string_of_id id2)^" is already used.");
         let sign' = rename_hyp id1 id2 sign in
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 962061f34..44c5d7f30 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -45,7 +45,7 @@ let current_proof_depth () =
 let undo_todepth n =
   try
     undo ((current_proof_depth ()) - n )
-  with Proof_global.NoCurrentProof  when n=0 -> ()
+  with Proof_global.NoCurrentProof  when Int.equal n 0 -> ()
 
 let start_proof id str hyps c ?init_tac ?compute_guard hook = 
   let goals = [ (Global.env_of_context hyps , c) ] in
diff --git a/proofs/proof.ml b/proofs/proof.ml
index bae5f1157..479ccabcc 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -29,6 +29,8 @@
      Therefore the undo stack stores action to be ran to undo.
 *)
 
+open Util
+
 type _focus_kind = int
 type 'a focus_kind = _focus_kind
 type focus_info = Obj.t
@@ -48,7 +50,7 @@ let new_focus_kind () =
   r
 
 (* Auxiliary function to define conditions. *)
-let check kind1 kind2 = kind1=kind2
+let check kind1 kind2 = Int.equal kind1 kind2
 
 (* To be authorized to unfocus one must meet the condition prescribed by
     the action which focused.*)
@@ -85,7 +87,7 @@ module Cond = struct
     | _ , Cannot e -> Cannot e
     | Strict, Strict -> Strict
     | _ , _ -> Loose
-  let kind e k0 k p = bool e (k0=k) k p 
+  let kind e k0 k p = bool e (Int.equal k0 k) k p 
   let pdone e k p = bool e (Proofview.finished p) k p
 end
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 25ed1f3e8..9cc726beb 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -14,6 +14,7 @@
 (*                                                                     *)
 (***********************************************************************)
 
+open Util
 open Pp
 open Names
 
@@ -102,7 +103,7 @@ let _ = Errors.register_handler begin function
 end
 let extract id l =
   let rec aux = function
-    | ((id',_) as np)::l when id_ord id id' = 0 -> (np,l)
+    | ((id',_) as np)::l when id_eq id id' -> (np,l)
     | np::l -> let (np', l) = aux l in (np' , np::l)
     | [] -> raise NoSuchProof
   in
@@ -154,7 +155,7 @@ let msg_proofs () =
     | l ->  (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++
                (pr_sequence Nameops.pr_id l) ++ str".")
 
-let there_is_a_proof () = !current_proof <> []
+let there_is_a_proof () = not (List.is_empty !current_proof)
 let there_are_pending_proofs () = there_is_a_proof ()
 let check_no_pending_proof () =
   if not (there_are_pending_proofs ()) then
@@ -222,7 +223,7 @@ end
 let start_proof  id str goals ?(compute_guard=[]) hook =
   begin
     List.iter begin fun (id_ex,_) ->
-      if Names.id_ord id id_ex = 0 then raise AlreadyExists
+      if Names.id_eq id id_ex then raise AlreadyExists
     end !current_proof
   end;
   let p = Proof.start goals in
@@ -307,6 +308,12 @@ module Bullet = struct
 
   type t = Vernacexpr.bullet
 
+  let bullet_eq b1 b2 = match b1, b2 with
+  | Vernacexpr.Dash, Vernacexpr.Dash -> true
+  | Vernacexpr.Star, Vernacexpr.Star -> true
+  | Vernacexpr.Plus, Vernacexpr.Plus -> true
+  | _ -> false
+
   type behavior = {
     name : string;
     put : Proof.proof -> t -> unit
@@ -338,7 +345,7 @@ module Bullet = struct
 
     let has_bullet bul pr =
       let rec has_bullet = function
-	| b'::_ when bul=b' -> true
+	| b'::_ when bullet_eq bul b' -> true
 	| _::l -> has_bullet l
 	| [] -> false
       in
@@ -358,7 +365,7 @@ module Bullet = struct
     let put p bul =
       if has_bullet bul p then
 	Proof.transaction p begin fun () ->
-	  while bul <> pop p do () done;
+	  while not (bullet_eq bul (pop p)) do () done;
 	  push bul p
 	end
       else
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 98e1acc42..a4b914525 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -20,6 +20,8 @@
    There is also need of a list of the evars which initialised the proofview
    to be able to return information about the proofview. *)
 
+open Util
+
 (* Type of proofviews. *)
 type proofview = {
      initial : (Term.constr * Term.types) list;
@@ -81,7 +83,7 @@ exception IndexOutOfRange
    Raises [IndexOutOfRange] if [i > length l]*)
 let list_goto = 
   let rec aux acc index = function
-    | l when index = 0-> (acc,l)
+    | l when Int.equal index 0-> (acc,l)
     | [] -> raise IndexOutOfRange
     | a::q -> aux (a::acc) (index-1) q
   in
@@ -313,7 +315,7 @@ let tclDISPATCHS tacs =
 let extend_to_list =
   let rec copy n x l =
     if n < 0 then raise SizeMismatch
-    else if n = 0 then l
+    else if Int.equal n 0 then l
     else copy (n-1) x (x::l)
   in
   fun startxs rx endxs l ->
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index c16e02b3f..aa3d13f8a 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -71,8 +71,8 @@ let map_strategy f l =
           match f q with
               Some q' -> q' :: ql
             | None -> ql) ql [] in
-      if ql'=[] then str else (lev,ql')::str) l [] in
-  if l'=[] then None else Some (false,l')
+      if List.is_empty ql' then str else (lev,ql')::str) l [] in
+  if List.is_empty l' then None else Some (false,l')
 
 let classify_strategy (local,_ as obj) =
   if local then Dispose else Substitute obj
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 78bdc194f..704dd9887 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -355,7 +355,7 @@ let tclIDTAC_list gls = gls
 
 let first_goal gls =
   let gl = gls.it and sig_0 = gls.sigma in
-  if gl = [] then error "first_goal";
+  if List.is_empty gl then error "first_goal";
   { it = List.hd gl; sigma = sig_0 }
 
 (* goal_goal_list : goal sigma -> goal list sigma *)
@@ -398,14 +398,15 @@ let check_evars env sigma extsigma gl =
   let origsigma = gl.sigma in
   let rest =
     Evd.fold_undefined (fun evk evi acc ->
-      if Evd.is_undefined extsigma evk & not (Evd.mem origsigma evk) then
+      if Evd.is_undefined extsigma evk && not (Evd.mem origsigma evk) then
 	evi::acc
       else
 	acc)
       sigma []
   in
-  if rest <> [] then
-    let evi = List.hd rest in
+  match rest with
+  | [] -> ()
+  | evi :: _ ->
     let (loc,k) = evi.evar_source in
     let evi = Evarutil.nf_evar_info sigma evi in
     Pretype_errors.error_unsolvable_implicit loc env sigma evi k None
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 0352d5624..66a9a9962 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -147,11 +147,11 @@ let convert_hyp_no_check d gl =
 
 (* This does not check dependencies *)
 let thin_no_check ids gl =
-  if ids = [] then tclIDTAC gl else refiner (Thin ids) gl
+  if List.is_empty ids then tclIDTAC gl else refiner (Thin ids) gl
 
 (* This does not check dependencies *)
 let thin_body_no_check ids gl =
-  if ids = [] then tclIDTAC gl else refiner (ThinBody ids) gl
+  if List.is_empty ids then tclIDTAC gl else refiner (ThinBody ids) gl
 
 let move_hyp_no_check with_dep id1 id2 gl =
   refiner (Move (with_dep,id1,id2)) gl
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 10ce0e76b..6f93ab725 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open Names
 open Pp
 open Tacexpr
@@ -69,11 +70,11 @@ let skip = ref 0
 let breakpoint = ref None
 
 let rec drop_spaces inst i =
-  if String.length inst > i && inst.[i] = ' ' then drop_spaces inst (i+1)
+  if String.length inst > i && inst.[i] == ' ' then drop_spaces inst (i+1)
   else i
 
 let possibly_unquote s =
-  if String.length s >= 2 & s.[0] = '"' & s.[String.length s - 1] = '"' then
+  if String.length s >= 2 & s.[0] == '"' & s.[String.length s - 1] == '"' then
     String.sub s 1 (String.length s - 2)
   else
     s
@@ -84,7 +85,7 @@ let db_initialize () =
 
 (* Gives the number of steps or next breakpoint of a run command *)
 let run_com inst =
-  if (String.get inst 0)='r' then
+  if (String.get inst 0) == 'r' then
     let i = drop_spaces inst 1 in
     if String.length inst > i then
       let s = String.sub inst i (String.length inst - i) in
@@ -135,10 +136,10 @@ let rec prompt level =
 let debug_prompt lev g tac f =
   (* What to print and to do next *)
   let newlevel =
-    if !skip = 0 then
-      if !breakpoint = None then (goal_com g tac; prompt lev)
+    if Int.equal !skip 0 then
+      if Option.is_empty !breakpoint then (goal_com g tac; prompt lev)
       else (run false; DebugOn (lev+1))
-    else (decr skip; run false; if !skip=0 then skipped:=0; DebugOn (lev+1)) in
+    else (decr skip; run false; if Int.equal !skip 0 then skipped:=0; DebugOn (lev+1)) in
   (* What to execute *)
   try f newlevel
   with e ->
@@ -147,14 +148,19 @@ let debug_prompt lev g tac f =
       msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error e);
     raise e
 
+let is_debug db = match db, !breakpoint with
+| DebugOff, _ -> false
+| _, Some _ -> false
+| _ -> Int.equal !skip 0
+
 (* Prints a constr *)
 let db_constr debug env c =
-  if debug <> DebugOff & !skip = 0 & !breakpoint = None then
+  if is_debug debug then
     msg_tac_debug (str "Evaluated term: " ++ print_constr_env env c)
 
 (* Prints the pattern rule *)
 let db_pattern_rule debug num r =
-  if debug <> DebugOff & !skip = 0 & !breakpoint = None then
+  if is_debug debug then
   begin
     msg_tac_debug (str "Pattern rule " ++ int num ++ str ":" ++ fnl () ++
       str "|" ++ spc () ++ !prmatchrl r)
@@ -167,38 +173,38 @@ let hyp_bound = function
 
 (* Prints a matched hypothesis *)
 let db_matched_hyp debug env (id,_,c) ido =
-  if debug <> DebugOff & !skip = 0 & !breakpoint = None then
+  if is_debug debug then
     msg_tac_debug (str "Hypothesis " ++
            str ((Names.string_of_id id)^(hyp_bound ido)^
                 " has been matched: ") ++ print_constr_env env c)
 
 (* Prints the matched conclusion *)
 let db_matched_concl debug env c =
-  if debug <> DebugOff & !skip = 0 & !breakpoint = None then
+  if is_debug debug then
     msg_tac_debug (str "Conclusion has been matched: " ++ print_constr_env env c)
 
 (* Prints a success message when the goal has been matched *)
 let db_mc_pattern_success debug =
-  if debug <> DebugOff & !skip = 0 & !breakpoint = None then
+  if is_debug debug then
     msg_tac_debug (str "The goal has been successfully matched!" ++ fnl() ++
            str "Let us execute the right-hand side part..." ++ fnl())
 
 (* Prints a failure message for an hypothesis pattern *)
 let db_hyp_pattern_failure debug env (na,hyp) =
-  if debug <> DebugOff & !skip = 0 & !breakpoint = None then
+  if is_debug debug then
     msg_tac_debug (str ("The pattern hypothesis"^(hyp_bound na)^
                 " cannot match: ") ++
            !prmatchpatt env hyp)
 
 (* Prints a matching failure message for a rule *)
 let db_matching_failure debug =
-  if debug <> DebugOff & !skip = 0 & !breakpoint = None then
+  if is_debug debug then
     msg_tac_debug (str "This rule has failed due to matching errors!" ++ fnl() ++
            str "Let us try the next one...")
 
 (* Prints an evaluation failure message for a rule *)
 let db_eval_failure debug s =
-  if debug <> DebugOff & !skip = 0 & !breakpoint = None then
+  if is_debug debug then
     let s = str "message \"" ++ s ++ str "\"" in
     msg_tac_debug
       (str "This rule has failed due to \"Fail\" tactic (" ++
@@ -206,7 +212,7 @@ let db_eval_failure debug s =
 
 (* Prints a logic failure message for a rule *)
 let db_logic_failure debug err =
-  if debug <> DebugOff & !skip = 0 & !breakpoint = None then
+  if is_debug debug then
   begin
     msg_tac_debug (!explain_logic_error err);
     msg_tac_debug (str "This rule has failed due to a logic error!" ++ fnl() ++
@@ -214,12 +220,12 @@ let db_logic_failure debug err =
   end
 
 let is_breakpoint brkname s = match brkname, s with
-  | Some s, MsgString s'::_ -> s = s'
+  | Some s, MsgString s'::_ -> String.equal s s'
   | _ -> false
 
 let db_breakpoint debug s =
   match debug with
-  | DebugOn lev when s <> [] & is_breakpoint !breakpoint s ->
+  | DebugOn lev when not (List.is_empty s) && is_breakpoint !breakpoint s ->
       breakpoint:=None
   | _ ->
       ()