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/string_notation.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/syntax/string_notation.ml')

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