diff options
| author | Pierre-Marie Pédrot | 2015-02-11 17:55:50 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-11 17:55:50 +0100 |
| commit | 37076a63ebd1491f26a6c5a3d67e054c106589b3 (patch) | |
| tree | 702d4be5c21408ce819b1265ac7cd4d5d2c2866d /stm | |
| parent | 956b7c4304582b1e9e3ca0bb34944bcbac18c0cc (diff) | |
| parent | ac65eef8bbc2e405f1964f35c6a129dfa1755888 (diff) | |
Merge branch 'v8.5'
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 3a57d85bab..96a11d306d 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 -> |