diff options
| author | Maxime Dénès | 2018-11-26 09:03:43 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-11-27 15:09:19 +0100 |
| commit | 37d92aa2b495a7208726f626693b819fd5695cc7 (patch) | |
| tree | aa1f8cedc4a8b3b2bc88f0f8a5811be128c79f01 /stm | |
| parent | 3bffd4f4f4a9ef400781aa7a4f90a986891bb0c1 (diff) | |
Make `-async-proofs on` effective with `coqc`
Before this patch, it had no effect.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 4 | ||||
| -rw-r--r-- | stm/stm.mli | 4 |
2 files changed, 5 insertions, 3 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 0969eb0918..3ae6b3a03e 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2643,13 +2643,14 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = name by looking at the load path! *) List.iter Mltop.add_coq_path iload_path; + Safe_typing.allow_delayed_constants := !cur_opt.async_proofs_mode <> APoff; + begin match doc_type with | Interactive ln -> let dp = match ln with | TopLogical dp -> dp | TopPhysical f -> dirpath_of_file f in - Safe_typing.allow_delayed_constants := true; Declaremods.start_library dp | VoDoc f -> @@ -2660,7 +2661,6 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = set_compilation_hints f | VioDoc f -> - Safe_typing.allow_delayed_constants := true; let ldir = dirpath_of_file f in check_coq_overwriting ldir; let () = Flags.verbosely Declaremods.start_library ldir in diff --git a/stm/stm.mli b/stm/stm.mli index 4db83a7359..b6071fa56b 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -16,7 +16,9 @@ open Names module AsyncOpts : sig type cache = Force - type async_proofs = APoff | APonLazy | APon + type async_proofs = APoff + | APonLazy (* Delays proof checking, but does it in master *) + | APon type tac_error_filter = [ `None | `Only of string list | `All ] type stm_opt = { |