From 675a1dc401eb9a5540ba5bc9a522c1f84d4c3d54 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 10 Jun 2017 04:57:03 +0200
Subject: [stm] [flags] Move document mode flags to the STM.

We move toplevel/STM flags from `Flags` to their proper components;
this ensures that low-level code doesn't depend on them, which was
incorrect and source of many problems wrt the interfaces.

Lower-level components should not be aware whether they are running in
batch or interactive mode, but instead provide a functional interface.

In particular:

== Added flags ==

- `Safe_typing.allow_delayed_constants`
  Allow delayed constants in the kernel.

- `Flags.record_aux_file`
  Output `Proof using` information from the kernel.

- `System.trust_file_cache`
  Assume that the file system won't change during our run.

== Deleted flags ==

- `Flags.compilation_mode`
- `Flags.batch_mode`

Additionally, we modify the STM entry point and `coqtop` to account
for the needed state. Note that testing may be necessary and the
number of combinations possible exceeds what the test-suite / regular
use does.

The next step is to fix the initialization problems [c.f. Bugzilla],
which will require a larger rework of the STM interface.
---
 kernel/term_typing.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'kernel/term_typing.ml')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 3f42c348fc..0c0b910e1d 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -428,13 +428,12 @@ let build_constant_declaration kn env result =
             let expr =
               !suggest_proof_using (Constant.to_string kn)
                 env vars ids_typ context_ids in
-            if !Flags.compilation_mode = Flags.BuildVo then
-              record_aux env ids_typ vars expr;
+            if !Flags.record_aux_file then record_aux env ids_typ vars expr;
             vars
         in
         keep_hyps env (Idset.union ids_typ ids_def), def
     | None ->
-        if !Flags.compilation_mode = Flags.BuildVo then
+        if !Flags.record_aux_file then
           record_aux env Id.Set.empty Id.Set.empty "";
         [], def (* Empty section context: no need to check *)
     | Some declared ->
@@ -614,7 +613,7 @@ let translate_local_def mb env id centry =
   let open Cooking in
   let decl = infer_declaration ~trust:mb env None (DefinitionEntry centry) in
   let typ = decl.cook_type in
-  if Option.is_empty decl.cook_context && !Flags.compilation_mode = Flags.BuildVo then begin
+  if Option.is_empty decl.cook_context && !Flags.record_aux_file then begin
     match decl.cook_body with
     | Undef _ -> ()
     | Def _ -> ()
-- 
cgit v1.2.3