[numeral notation] Add support for parameterized inductives

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;