diff options
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index 44143e392f..012aaac8f0 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -164,8 +164,10 @@ type 'target conversion_kind = 'target * option_kind are translated acording to [args] where [ToPostCopy] means that the argument is kept unchanged and [ToPostAs k] means that the argument is recursively translated according to [l_k]. + [ToPostHole] introduces an additional implicit argument hole + (in the reverse translation, the corresponding argument is removed). When [n] is null, no translation is performed. *) -type to_post_arg = ToPostCopy | ToPostAs of int +type to_post_arg = ToPostCopy | ToPostAs of int | ToPostHole type ('target, 'warning) prim_token_notation_obj = { to_kind : 'target conversion_kind; to_ty : GlobRef.t; |