diff options
| -rw-r--r-- | toplevel/vernacentries.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 72dd967b92..ee11d356d1 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -34,8 +34,8 @@ open Misctypes open Locality let debug = false -let prerr_endline = - if debug then prerr_endline else fun _ -> () +let prerr_endline x = + if debug then prerr_endline (x ()) else () (* Misc *) @@ -1841,7 +1841,7 @@ let vernac_load interp fname = * still parsed as the obsolete_locality grammar entry for retrocompatibility. * loc is the Loc.t of the vernacular command being interpreted. *) let interp ?proof ~loc locality poly c = - prerr_endline ("interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c)); + prerr_endline (fun () -> "interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c)); match c with (* Done later in this file *) | VernacLoad _ -> assert false |