Library Ltac2.Printf

This file defines a printf notation for easiness of writing messages The built-in "format" notation scope can be used to create well-typed variadic printing commands following a printf-like syntax. The "format" scope parses quoted strings which contain either raw string data or printing specifications. Raw strings will be output verbatim as if they were passed to Ltac2.Message.of_string. Printing specifications are of the form '%' type where the type value defines which kind of arguments will be accepted and how they will be printed. They can take the following values.

• i : takes an argument of type int and behaves as Message.of_int
• I : takes an argument of type ident and behaves as Message.of_ident
• s : takes an argument of type string and behaves as Message.of_string
• m : takes an argument of type message and prints it unmodified
• t : takes an argument of type constr and behaves as Message.of_constr
• a : takes two arguments f of type (unit -> 'a -> message) and x of type 'a and behaves as f () x
• A : takes two arguments f of type ('a -> message) and x of type 'a and behaves as f x
• % : outputs % verbatim

TODO: add printing modifiers.

The two following notations are made available when this module is imported.

• printf will parse a format and generate a function taking the corresponding arguments ant printing the resulting message as per Message.print. In particular when fully applied it has type unit.
• fprintf behaves similarly but return the message as a value instead of printing it.