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 012aaac8f0..acca7b262b 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -166,8 +166,10 @@ type 'target conversion_kind = 'target * option_kind argument is recursively translated according to [l_k]. [ToPostHole] introduces an additional implicit argument hole (in the reverse translation, the corresponding argument is removed). + [ToPostCheck r] behaves as [ToPostCopy] except in the reverse + translation which fails if the copied term is not [r]. When [n] is null, no translation is performed. *) -type to_post_arg = ToPostCopy | ToPostAs of int | ToPostHole +type to_post_arg = ToPostCopy | ToPostAs of int | ToPostHole | ToPostCheck of GlobRef.t type ('target, 'warning) prim_token_notation_obj = { to_kind : 'target conversion_kind; to_ty : GlobRef.t; |