[numeral notation] Allow to put/ignore holes during pre/postprocessing

This will enable to handle implicit arguments by ignoring them during
preprocessing (before uninterpreting (i.e., printing)) and remplace
them with holes `_` during postprocessing (after interpreting (i.e.,
parsing)).

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;