diff options
| -rw-r--r-- | toplevel/vernacentries.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 90689aee6f..fb50a6bc22 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -485,7 +485,8 @@ let qed_display_script = ref true let vernac_end_proof ?proof = function | Admitted -> save_proof ?proof Admitted | Proved (_,_) as e -> - if is_verbose () && !qed_display_script then Stm.show_script ?proof (); + if is_verbose () && !qed_display_script && !Flags.coqtop_ui then + Stm.show_script ?proof (); save_proof ?proof e (* A stupid macro that should be replaced by ``Exact c. Save.'' all along |