diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-19 11:11:50 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-19 11:11:50 +0100 |
| commit | 073b92396a68be30f77c80960a58ca562bb01f49 (patch) | |
| tree | d2ad366f28624196ebfe9c1eadf595dcb490fcdc /dev/base_include | |
| parent | c047ecce6e4dba33df69a53a9e168999676c65db (diff) | |
| parent | ed18f926e4695acc730218925ca156abe56ba5fc (diff) | |
Merge PR #6753: [toplevel] Make toplevel state into a record.
Diffstat (limited to 'dev/base_include')
| -rw-r--r-- | dev/base_include | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/base_include b/dev/base_include index 320d366aa..350ccaa10 100644 --- a/dev/base_include +++ b/dev/base_include @@ -229,7 +229,7 @@ let _ = Flags.in_toplevel := true let _ = Constrextern.set_extern_reference (fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Id.Set.empty r));; -let go () = Coqloop.loop Option.(get !Coqtop.drop_last_doc) +let go () = Coqloop.loop ~time:false ~state:Option.(get !Coqtop.drop_last_doc) let _ = print_string |