From 13f962c7a96bdc402812ae850cc3e36bc59e45af Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 25 May 2004 20:57:19 +0000
Subject: Correction bug 'Time Load foo'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5759 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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)
-- 
cgit v1.2.3