From da72fafac3b5b4b21330cd097f5728cbc127aea4 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Sat, 12 Sep 2020 09:15:06 +0200
Subject: Renaming Numeral into Number

---
 plugins/syntax/int63_syntax.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/plugins/syntax/int63_syntax.ml b/plugins/syntax/int63_syntax.ml
index 5f4db8e800..73a9341145 100644
--- a/plugins/syntax/int63_syntax.ml
+++ b/plugins/syntax/int63_syntax.ml
@@ -50,7 +50,7 @@ let _ =
        enable_prim_token_interpretation
          { pt_local = false;
            pt_scope = int63_scope;
-           pt_interp_info = NumeralNotation o;
+           pt_interp_info = NumberNotation o;
            pt_required = (int63_path, int63_module);
            pt_refs = [];
            pt_in_match = false })
-- 
cgit v1.2.3


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

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

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