diff options
author | 2015-02-08 10:20:39 +0100 | |
---|---|---|
committer | 2015-02-10 21:56:06 +0100 | |
commit | f804e681f1550e1c20b8ce5b83bc66c876fb3c99 (patch) | |
tree | d112771be4296cd091b3e2128e8603487bac2420 /stm/stm.ml | |
parent | 02d2cdf61f6c6a37a1bda25d738a0d189a4021a6 (diff) |
Improving further e11854569b8 and 3e5b9ab9f75e4 on when to print goals in coqtop mode.
Diffstat (limited to 'stm/stm.ml')
-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 3a57d85ba..96a11d306 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2278,7 +2278,7 @@ let interp verb (_,e as lexpr) = let print_goals = verb && match clas with | VtQuery _, _ -> false - | (VtProofStep _ | VtStm (VtBack _, _)), _ -> true + | (VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _), _ -> true | _ -> not !Flags.coqtop_ui || !Flags.print_emacs in try finish ~print_goals () with e -> |