diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/profile_ltac.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/tactic_debug.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 243e0e945c..9d46bbc74e 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -376,7 +376,7 @@ let get_local_profiling_results () = List.hd Local.(!stack) own. *) module DData = struct type t = Feedback.doc_id * Stateid.t - let compare x y = Pervasives.compare x y + let compare x y = compare x y end module SM = Map.Make(DData) diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 9e735e0680..539536911c 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -156,7 +156,7 @@ let rec prompt level = begin let open Proofview.NonLogical in Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >> - if Pervasives.(!batch) then return (DebugOn (level+1)) else + if Util.(!batch) then return (DebugOn (level+1)) else let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in Proofview.NonLogical.catch Proofview.NonLogical.read_line begin function (e, info) -> match e with |