diff options
Diffstat (limited to 'toplevel/obligations.ml')
| -rw-r--r-- | toplevel/obligations.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 6277faf27..5210a3c9e 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -149,7 +149,7 @@ let trunc_named_context n ctx = List.firstn (len - n) ctx let rec chop_product n t = - if n = 0 then Some t + if Int.equal n 0 then Some t else match kind_of_term t with | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None @@ -645,7 +645,7 @@ let get_prog_err n = let get_any_prog_err () = try get_any_prog () with NoObligations id -> pperror (explain_no_obligations id) -let obligations_solved prg = (snd prg.prg_obligations) = 0 +let obligations_solved prg = Int.equal (snd prg.prg_obligations) 0 let all_programs () = ProgMap.fold (fun k p l -> p :: l) !from_prg [] @@ -657,7 +657,7 @@ type progress = let obligations_message rem = if rem > 0 then - if rem = 1 then + if Int.equal rem 1 then Flags.if_verbose msg_info (int rem ++ str " obligation remaining") else Flags.if_verbose msg_info (int rem ++ str " obligations remaining") @@ -898,7 +898,7 @@ let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic let info = str (string_of_id n) ++ str " has type-checked" in let prg = init_prog_info n term t [] None [] obls implicits kind reduce hook in let obls,_ = prg.prg_obligations in - if Array.length obls = 0 then ( + if Int.equal (Array.length obls) 0 then ( Flags.if_verbose msg_info (info ++ str "."); let cst = declare_definition prg in Defined cst) |