diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-11-27 16:55:05 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-27 16:55:05 +0100 |
| commit | 68061d8d464d0c62442675897c9c5f6db8d2b2e4 (patch) | |
| tree | d0b0b312054b505a5bd5d1c9da71de70f9cc2f93 /toplevel | |
| parent | 2fcbfcfe8066bcf7ee40830bb9043b0cfd754e63 (diff) | |
| parent | 83c63a5075fb55e4e3291e163417bcffaf009dcd (diff) | |
Merge PR #6207: [stm] Allow delayed constant in interactive mode.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c61a1fd41..553da2dc0 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -333,8 +333,8 @@ let compile ~verbosely ~f_in ~f_out = (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); Aux_file.stop_aux_file (); Dumpglob.end_dump_glob () - | BuildVio -> + | BuildVio -> Flags.record_aux_file := false; Dumpglob.noglob (); @@ -734,9 +734,7 @@ let parse_args arglist = |"-profile-ltac" -> Flags.profile_ltac := true |"-q" -> Coqinit.no_load_rc () |"-quiet"|"-silent" -> Flags.quiet := true; Flags.make_warn false - |"-quick" -> - Safe_typing.allow_delayed_constants := true; - compilation_mode := BuildVio + |"-quick" -> compilation_mode := BuildVio |"-list-tags" -> print_tags := true |"-time" -> Flags.time := true |"-type-in-type" -> set_type_in_type () |