]> matita.cs.unibo.it Git - helm.git/commitdiff
fixed a typo
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 29 Apr 2005 12:09:33 +0000 (12:09 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 29 Apr 2005 12:09:33 +0000 (12:09 +0000)
helm/ocaml/metadata/test.ml

index 0264681bc05f18005748ea0ea5d2dfb86504bbc9..43b29e4b6cc671087e56ef6cc35e4cdb2362cfd6 100644 (file)
@@ -39,6 +39,7 @@ end else
   with 
   | _ -> 
     prerr_endline 
-      ("total persing time " ^ (string_of_float !CicEnvironment.total_time)); 
+      ("total persing time " ^ 
+         (string_of_float !CicEnvironment.total_prasing_time)); 
     close_in ic