diff options
| author | Emilio Jesus Gallego Arias | 2019-01-29 00:44:34 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-01-30 13:41:08 +0100 |
| commit | d9fb8db86d5b4ddc79a207c5f0ac32eb98215e78 (patch) | |
| tree | 12c39326849f9491b5bf34f20a1aa4cb165e3933 /stm | |
| parent | 469032d0274812cbf00823f86fc3db3a1204647e (diff) | |
[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.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |