diff options
Diffstat (limited to 'user-contrib/Ltac2/tac2print.mli')
| -rw-r--r-- | user-contrib/Ltac2/tac2print.mli | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/user-contrib/Ltac2/tac2print.mli b/user-contrib/Ltac2/tac2print.mli index df5b03f82a..6bb4884666 100644 --- a/user-contrib/Ltac2/tac2print.mli +++ b/user-contrib/Ltac2/tac2print.mli @@ -46,3 +46,19 @@ val pr_valexpr : Environ.env -> Evd.evar_map -> valexpr -> 'a glb_typexpr -> Pp. val int_name : unit -> (int -> string) (** Create a function that give names to integers. The names are generated on the fly, in the order they are encountered. *) + +(** {5 Ltac2 primitives}*) + +type format = +| FmtString +| FmtInt +| FmtConstr +| FmtIdent +| FmtLiteral of string +| FmtAlpha + +val val_format : format list Tac2dyn.Val.tag + +exception InvalidFormat + +val parse_format : string -> format list |