diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-10-31 14:43:04 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-10-31 15:54:00 +0100 |
| commit | baef2bd34e1906ab56918c37a90c5468a4785656 (patch) | |
| tree | dda40ffcff58cedeacc45ae6d79fda6e0774e3e2 /toplevel/vernacentries.ml | |
| parent | b4c8a7ead01ac81575530e36386a58f49432b35f (diff) | |
Show_script called only if in coqtop mode
Diffstat (limited to 'toplevel/vernacentries.ml')
| -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 90689aee6..fb50a6bc2 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 |