From dfcb15141a19db4f1cc61c14d1cdad0275009356 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 3 Sep 2020 13:11:00 +0200
Subject: [numeral notation] Add a pre/postprocessing

This will enable to define numeral notation on non inductive by using
an inductive type as proxy and those translations to translate to/from
the actual type to the inductive type.
---
 plugins/syntax/int63_syntax.ml    | 1 +
 plugins/syntax/numeral.ml         | 2 +-
 plugins/syntax/string_notation.ml | 1 +
 3 files changed, 3 insertions(+), 1 deletion(-)

(limited to 'plugins/syntax')

diff --git a/plugins/syntax/int63_syntax.ml b/plugins/syntax/int63_syntax.ml
index 73a9341145..b14b02f3bb 100644
--- a/plugins/syntax/int63_syntax.ml
+++ b/plugins/syntax/int63_syntax.ml
@@ -43,6 +43,7 @@ let _ =
        let id_int63 = Nametab.locate q_id_int63 in
        let o = { to_kind = Int63, Direct;
                  to_ty = id_int63;
+                 to_post = [||];
                  of_kind = Int63, Direct;
                  of_ty = id_int63;
                  ty_name = q_int63;
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index 8635f39f1a..ad90a9a982 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -199,7 +199,7 @@ let vernac_number_notation local ty f g scope opts =
    | _, ((DecimalInt _ | DecimalUInt _ | Decimal _), _) ->
       warn_deprecated_decimal ()
    | _ -> ());
-  let o = { to_kind; to_ty; of_kind; of_ty;
+  let o = { to_kind; to_ty; to_post = [||]; of_kind; of_ty;
             ty_name = ty;
             warning = opts }
   in
diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml
index e7ed0d8061..dbb0e92d5c 100644
--- a/plugins/syntax/string_notation.ml
+++ b/plugins/syntax/string_notation.ml
@@ -82,6 +82,7 @@ let vernac_string_notation local ty f g scope =
   in
   let o = { to_kind = to_kind;
             to_ty = to_ty;
+            to_post = [||];
             of_kind = of_kind;
             of_ty = of_ty;
             ty_name = ty;
-- 
cgit v1.2.3