[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.

1 files changed, 2 insertions, 2 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 1d5406770..8f676c656 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -32,7 +32,7 @@ let load_rcfile sid =
     try
       if !rcfile_specified then
         if CUnix.file_readable_p !rcfile then
-          Vernac.load_vernac false sid !rcfile
+          Vernac.load_vernac ~verbosely:false ~interactive:false ~check:true sid !rcfile
         else raise (Sys_error ("Cannot read rcfile: "^ !rcfile))
       else
 	try
@@ -43,7 +43,7 @@ let load_rcfile sid =
 	    Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version;
 	    Envars.home ~warn / "."^rcdefaultname
 	  ] in
-          Vernac.load_vernac false sid inferedrc
+          Vernac.load_vernac ~verbosely:false ~interactive:false ~check:true sid inferedrc
 	with Not_found -> sid
 	(*
 	Flags.if_verbose