diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-06 17:51:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-06 17:51:57 +0200 |
| commit | c4db6fc1086d984fd983ff9a6797ad108d220b98 (patch) | |
| tree | cb57e5b678218e2baad13184544e645fd2e22cf5 /engine/logic_monad.ml | |
| parent | 944c8de0bfe4048e0733a487e6388db4dfc9075a (diff) | |
| parent | 840155eafd9607c7656c80770de1e2819fe56a13 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'engine/logic_monad.ml')
| -rw-r--r-- | engine/logic_monad.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index c88de133d..47a5510b0 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -95,7 +95,11 @@ struct let print_char = fun c -> (); fun () -> print_char c (** {!Pp.pp}. The buffer is also flushed. *) - let print = fun s -> (); fun () -> try Pp.msg_info s; Pp.pp_flush () with e -> + let print_debug = fun s -> (); fun () -> try Pp.msg_info s; Pp.pp_flush () with e -> + let (e, info) = Errors.push e in raise ~info e () + + (** {!Pp.pp}. The buffer is also flushed. *) + let print = fun s -> (); fun () -> try Pp.msg_notice s; Pp.pp_flush () with e -> let (e, info) = Errors.push e in raise ~info e () let timeout = fun n t -> (); fun () -> |