The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

You can insert two linebreaks by guessing a value for the widest buffer your users will have, and insert that many spaces, like:

fail 0 "aasdf" "                                                                                                    " "adsf".

If you can accept extra quotations, and a possible %string if string_scope is closed, you can do

Require Import Coq.Strings.String.

Local Open Scope string_scope.

Definition NEWLINE := String (Ascii.Ascii false true false true false false false false) EmptyString.

Goal True.

  let nl := (eval unfold NEWLINE in NEWLINE) in

  fail 0 "asdf" nl "asdf".

 

On Fri, Mar 27, 2015 at 6:52 PM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

Is there any way to compose a single fail message from multiple strings and terms with explicit line breaks inserted at certain points?  I tried "\n" (eg. below) and various direct ascii characters, but they all just printed out without being interpreted as line breaks.  Also, putting the fail args on separate lines doesn't change things.

  fail 0 "mytactic failure:" term1 "\ndid not work with" term2


-- Jonathan