diff options
author | 2017-11-21 13:14:17 +0100 | |
---|---|---|
committer | 2017-11-21 13:14:17 +0100 | |
commit | 83c63a5075fb55e4e3291e163417bcffaf009dcd (patch) | |
tree | 31686304f831584f322dd6d143956a57ea917e20 | |
parent | 2a857da2a88855a6c9f0fa7e48a8700c1613e0c7 (diff) |
[stm] Allow delayed constant in interactive mode.
This setting is a debug assertion, due to the many flags we still
over-approximate setting the flag to true to all interactive
environments. [So the assert is checked in vo compilation]
Fixes #6152.
-rw-r--r-- | stm/stm.ml | 4 | ||||
-rw-r--r-- | toplevel/coqtop.ml | 6 |
2 files changed, 6 insertions, 4 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 864fff9e0..359890eb7 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2478,12 +2478,16 @@ let new_doc { doc_type ; require_libs } = begin match doc_type with | Interactive ln -> + Safe_typing.allow_delayed_constants := true; Declaremods.start_library ln + | VoDoc ln -> let ldir = Flags.verbosely Library.start_library ln in VCS.set_ldir ldir; set_compilation_hints ln + | VioDoc ln -> + Safe_typing.allow_delayed_constants := true; let ldir = Flags.verbosely Library.start_library ln in VCS.set_ldir ldir; set_compilation_hints ln diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index f3d5d9b85..a840cbc50 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 () |