From d9fb8db86d5b4ddc79a207c5f0ac32eb98215e78 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 29 Jan 2019 00:44:34 +0100
Subject: [toplevel] Deprecate the `-compile` flag in favor of `coqc`.

This PR deprecates the use of `coqtop` as a compiler.

There is no point on having two binaries with the same purpose; after
the experiment in #8690, IMHO we have a lot to gain in terms of code
organization by splitting the compiler and the interactive binary.

We adapt the documentation and adapt the test-suite.

Note that we don't make `coqc` a true binary yet, but here we take
care only of the user-facing part.

The conversion of the binary will take place in #8690 and will bring
code simplification, including a unified handling of arguments.
---
 stm/stm.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index dfe5581ed5..0165b3c029 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1671,7 +1671,7 @@ end = struct (* {{{ *)
         when is_tac expr && State.same_env o n -> (* A pure tactic *)
           Some (id, `ProofOnly (prev, State.proof_part_of_frozen n))
       | Some _, Some s ->
-          msg_debug (Pp.str "STM: sending back a fat state");
+        if !Flags.debug then msg_debug (Pp.str "STM: sending back a fat state");
           Some (id, `Full s)
       | _, Some s -> Some (id, `Full s) in
     let rec aux seen = function
-- 
cgit v1.2.3