aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-06-02 14:35:13 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-06-02 14:35:13 +0200
commit13e8983e3be6bff993c212d7fdcf707cf3c749c6 (patch)
tree46ad587ecdbf12e7cd047e9f2029b81db347a9c2 /proofs
parent129faf2dbd68e0f3ab8688496372b6406e3ee2e4 (diff)
parent6b041a242607ec906fbab451e53c15af6339e4ef (diff)
Merge PR#647: [emacs] [toplevel] Make emacs flag local to the toplevel.
Diffstat (limited to 'proofs')
-rw-r--r--proofs/refiner.ml6
1 files changed, 2 insertions, 4 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 259e96a27..91e6dc4ab 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -188,8 +188,6 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
(fun hypl -> List.subtract cmp hypl oldhyps)
hyps
in
- let emacs_str s =
- if !Flags.print_emacs then s else "" in
let s =
let frst = ref true in
List.fold_left
@@ -199,9 +197,9 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
"" lh))
"" newhyps in
Feedback.msg_notice
- (str (emacs_str "<infoH>")
+ (str "<infoH>"
++ (hov 0 (str s))
- ++ (str (emacs_str "</infoH>")));
+ ++ (str "</infoH>"));
tclIDTAC goal;;