diff --git a/doc/invargent-manual.pdf b/doc/invargent-manual.pdf
index 43f77df..8e74ed6 100644
Binary files a/doc/invargent-manual.pdf and b/doc/invargent-manual.pdf differ
diff --git a/doc/invargent-manual.tm b/doc/invargent-manual.tm
index c2f8604..f605a45 100644
--- a/doc/invargent-manual.tm
+++ b/doc/invargent-manual.tm
@@ -697,6 +697,9 @@
     <item*|<verbatim|-inform>>Print type schemes of toplevel definitions as
     they are inferred.
 
+    <item*|<verbatim|-time>>Print the time it took to infer type schemes of
+    toplevel definitions.
+
     <item*|<verbatim|-no_sig>>Do not generate the <verbatim|.gadti> file.
 
     <item*|<verbatim|-no_ml>>Do not generate the <verbatim|.ml> file.
diff --git a/src/Infer.ml b/src/Infer.ml
index 131c581..3370a4d 100644
--- a/src/Infer.ml
+++ b/src/Infer.ml
@@ -9,6 +9,7 @@
 let annotating_fun = ref true
 let annotating_letin = ref false
 let inform_toplevel = ref false
+let time_toplevel = ref false
 let merge_rec_nonrec = ref true
 
 open Defs
@@ -744,6 +745,8 @@ let prepare_scheme phi res =
   VarSet.union vs rvs, phi
 
 let infer_prog solver prog =
+  let ntime = ref (Sys.time ()) in
+  let start_time = !ntime in
   let gamma = ref [] in
   let update_new_ex_types q new_ex_types sb sb_chi =
     let more_items = ref [] in
@@ -851,6 +854,11 @@ let infer_prog solver prog =
           if !inform_toplevel
           then Format.printf
               "@[<2>val@ %s :@ %a@]@\n%!" x pr_typscheme typ_sch;
+          if !inform_toplevel && !time_toplevel
+          then (
+            let time = Sys.time () in
+            Format.printf "(t=%.3fs)@\n" (time -. !ntime);
+            ntime := time);
           (match pat_loc with
            | Some lc ->
              ex_items @
@@ -931,6 +939,11 @@ let infer_prog solver prog =
               if !inform_toplevel
               then Format.printf
                   "@[<2>val@ %s :@ %a@]@\n%!" x pr_typscheme typ_sch;
+              if !inform_toplevel && !time_toplevel
+              then (
+                let time = Sys.time () in
+                Format.printf "(t=%.3fs)@\n" (time -. !ntime);
+                ntime := time);
               x, typ_sch
             else fun (x, res) ->
               let res = subst_typ exsb res in
@@ -970,12 +983,19 @@ let infer_prog solver prog =
               if !inform_toplevel
               then Format.printf
                   "@[<2>val@ %s :@ %a@]@\n%!" x pr_typscheme typ_sch;  
+              if !inform_toplevel && !time_toplevel
+              then (
+                let time = Sys.time () in
+                Format.printf "(t=%.3fs)@\n" (time -. !ntime);
+                ntime := time);
               x, typ_sch in
           let typ_schs = List.map typ_sch_ex env in
           gamma := typ_schs @ !gamma;
           ex_items @ List.rev !more_items
           @ [ILetVal (docu, p, e, top_sch, typ_schs, tests, elim_extypes, loc)]
       ) prog in
+  if !time_toplevel
+  then Format.printf "@\nTotal time %.3fs@\n" (Sys.time () -. start_time);
   List.rev !gamma, items
 
 
diff --git a/src/Infer.mli b/src/Infer.mli
index 6a7f022..43df001 100644
--- a/src/Infer.mli
+++ b/src/Infer.mli
@@ -9,6 +9,7 @@
 val annotating_fun : bool ref
 val annotating_letin : bool ref
 val inform_toplevel : bool ref
+val time_toplevel : bool ref
 
 (** Each disjunct stores a trigger to be called when other disjuncts
     are eliminated during normalization-simplification. *)
diff --git a/src/InvarGenT.ml b/src/InvarGenT.ml
index b8fd864..eff45f9 100644
--- a/src/InvarGenT.ml
+++ b/src/InvarGenT.ml
@@ -73,6 +73,8 @@ let main () =
   let cli = [
     "-inform", Arg.Set Infer.inform_toplevel,
     "Print type schemes of toplevel definitions as they are inferred";
+    "-time", Arg.Set Infer.time_toplevel,
+    "Print the time it took to infer type schemes of toplevel definitions";
     "-no_sig", Arg.Clear do_sig,
     "Do not generate the `.gadti` file";
     "-no_ml", Arg.Clear do_ml,