aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacinterp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tacinterp.ml')
-rw-r--r--tactics/tacinterp.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index dd937cf6a..bbeb23c78 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1125,7 +1125,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
let msgnl =
let open Ftactic in
interp_message ist s >>= fun msg ->
- return (hov 0 msg , hov 0 msg ++ fnl ())
+ return (hov 0 msg , hov 0 msg)
in
let print (_,msgnl) = Proofview.(tclLIFT (NonLogical.print msgnl)) in
let log (msg,_) = Proofview.Trace.log (fun () -> msg) in