From 9082af80f5bb70ff2b75117f9e5cc3165b1c8b42 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 3 Sep 2020 13:22:00 +0200
Subject: [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)).
---
 interp/notation.mli | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'interp/notation.mli')

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;
-- 
cgit v1.2.3