diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-08-17 09:33:03 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-08-17 09:33:03 +0200 |
| commit | 8e79ac5a766e42dfbfc629087455c9bd7639402c (patch) | |
| tree | 95e7c9438c82574570fec1b1074a2a2a6a37e7ff /proofs | |
| parent | 6c65822cd241ea2f5c552f8b685490aed86eecb1 (diff) | |
infoH: output via msg_* to make the XML protocol happy
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/refiner.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 14493458c..ef4cfb158 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -218,7 +218,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) (fun acc (nm,_,_) -> (Names.Id.to_string nm) ^ " " ^ acc) "" lh)) "" newhyps in - pp (str (emacs_str "<infoH>") + msg_notice (str (emacs_str "<infoH>") ++ (hov 0 (str s)) ++ (str (emacs_str "</infoH>")) ++ fnl()); tclIDTAC goal;; |