diff options
| -rw-r--r-- | toplevel/vernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 2607ca4117..931b6578b2 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -195,7 +195,7 @@ let rec vernac_com interpfun (loc,com) = | VernacTime v -> let tstart = System.get_time() in - if not !just_parsing then interpfun v; + if not !just_parsing then interp v; let tend = System.get_time() in msgnl (str"Finished transaction in " ++ System.fmt_time_difference tstart tend) |