From 37d92aa2b495a7208726f626693b819fd5695cc7 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 26 Nov 2018 09:03:43 +0100
Subject: Make `-async-proofs on` effective with `coqc`

Before this patch, it had no effect.
---
 stm/stm.ml  | 4 ++--
 stm/stm.mli | 4 +++-
 2 files changed, 5 insertions(+), 3 deletions(-)

(limited to 'stm')

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 = {
-- 
cgit v1.2.3