diff options
| author | Hugo Herbelin | 2014-12-06 15:51:40 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-12-07 15:14:38 +0100 |
| commit | 3e5b9ab9f75e4102068230769861fc875be0e306 (patch) | |
| tree | 2444de98fb62e84db814b4838457f6146fd85b23 | |
| parent | e4f9b2a8af4489b9d7fb27dcd2f919a54491c402 (diff) | |
Improving e11854569b8 on when to print goals in coqtop mode.
| -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 94987bdb91..6babc3e42f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2324,7 +2324,7 @@ let interp verb (_,e as lexpr) = let print_goals = verb && match clas with | VtQuery _, _ -> false - | VtProofStep _, _ -> true + | (VtProofStep _ | VtStm (VtBack _, _)), _ -> true | _ -> not !Flags.coqtop_ui || !Flags.print_emacs in try finish ~print_goals () with e -> |