diff options
| author | Arnaud Spiwack | 2014-09-24 09:39:09 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-09-24 09:39:09 +0200 |
| commit | c6863a4cf8a9ec4bc91335f59f3094974f01dd13 (patch) | |
| tree | bf56b5eaad1bef9ffa2c7d839b1786935911b508 | |
| parent | cc9618ef7543566013f4c9831df25f9503527507 (diff) | |
Fix a message.
| -rw-r--r-- | printing/printer.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index bb1c2dab95..b12aea5dbf 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -611,7 +611,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = | [] , [] , _ -> (* emacs mode: xml-like flag for detecting information message *) str (emacs_str "<infomsg>") ++ - str "No more, however there are goals you gave up. You need to go back and solve them." + str "No more goals, however there are goals you gave up. You need to go back and solve them." ++ str (emacs_str "</infomsg>") ++ fnl () ++ fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] given_up |