diff options
Diffstat (limited to 'user-contrib/Ltac2/Message.v')
| -rw-r--r-- | user-contrib/Ltac2/Message.v | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/user-contrib/Ltac2/Message.v b/user-contrib/Ltac2/Message.v index 4a4d1d815c..39d39562cf 100644 --- a/user-contrib/Ltac2/Message.v +++ b/user-contrib/Ltac2/Message.v @@ -25,3 +25,32 @@ Ltac2 @ external of_exn : exn -> message := "ltac2" "message_of_exn". (** Panics if there is more than one goal under focus. *) Ltac2 @ external concat : message -> message -> message := "ltac2" "message_concat". + +Module Format. + +(** Only for internal use. *) + +Ltac2 @ external stop : unit -> ('a, 'b, 'c, 'a) format := "ltac2" "format_stop". + +Ltac2 @ external string : ('a, 'b, 'c, 'd) format -> + (string -> 'a, 'b, 'c, 'd) format := "ltac2" "format_string". + +Ltac2 @ external int : ('a, 'b, 'c, 'd) format -> + (int -> 'a, 'b, 'c, 'd) format := "ltac2" "format_int". + +Ltac2 @ external constr : ('a, 'b, 'c, 'd) format -> + (constr -> 'a, 'b, 'c, 'd) format := "ltac2" "format_constr". + +Ltac2 @ external ident : ('a, 'b, 'c, 'd) format -> + (ident -> 'a, 'b, 'c, 'd) format := "ltac2" "format_ident". + +Ltac2 @ external literal : string -> ('a, 'b, 'c, 'd) format -> + ('a, 'b, 'c, 'd) format := "ltac2" "format_literal". + +Ltac2 @ external alpha : ('a, 'b, 'c, 'd) format -> + (('b -> 'r -> 'c) -> 'r -> 'a, 'b, 'c, 'd) format := "ltac2" "format_alpha". + +Ltac2 @ external kfprintf : (message -> 'r) -> ('a, unit, message, 'r) format -> 'a := + "ltac2" "format_kfprintf". + +End Format. |