From a9d24cf456dcd3cf4074fb719e5dd4676a548028 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= <pierre-marie.pedrot@inria.fr>
Date: Tue, 13 Feb 2024 09:29:47 +0100
Subject: [PATCH] Adapt w.r.t. coq/coq#18667.

---
 plugin/bignums_syntax.ml | 23 ++++++++++++++++-------
 1 file changed, 16 insertions(+), 7 deletions(-)

diff --git a/plugin/bignums_syntax.ml b/plugin/bignums_syntax.ml
index da930bc..568b91b 100644
--- a/plugin/bignums_syntax.ml
+++ b/plugin/bignums_syntax.ml
@@ -189,16 +189,26 @@ let uninterp_bigN (AnyGlobConstr rc) =
 let bigN_list_of_constructors =
   let rec build i =
     if i < n_inlined+1 then
-      (DAst.make @@ GRef (bigN_constructor i,None))::(build (i+1))
+      (bigN_constructor i)::(build (i+1))
     else
       []
   in
   build 0
 
+let declare_numeral_interpreter uid sc dir interp (patl,uninterp,b) =
+  let open Notation in
+  register_bignumeral_interpretation uid (interp,uninterp);
+  { pt_local = false;
+    pt_scope = sc;
+    pt_interp_info = Uid uid;
+    pt_required = dir;
+    pt_refs = patl;
+    pt_in_match = b }
+
 (* Actually declares the interpreter for bigN *)
 let _ =
   Notation.declare_scope bigN_scope;
-  Notation.declare_numeral_interpreter bigN_scope
+  declare_numeral_interpreter "bignums.bigN" bigN_scope
     (bigN_path, bigN_module)
     interp_bigN
     (bigN_list_of_constructors,
@@ -236,11 +246,10 @@ let uninterp_bigZ (AnyGlobConstr rc) =
 (* Actually declares the interpreter for bigZ *)
 let _ =
   Notation.declare_scope bigZ_scope;
-  Notation.declare_numeral_interpreter bigZ_scope
+  declare_numeral_interpreter "bignums.bigZ" bigZ_scope
     (bigZ_path, bigZ_module)
     interp_bigZ
-    ([DAst.make @@ GRef (bigZ_pos, None);
-      DAst.make @@ GRef (bigZ_neg, None)],
+    ([bigZ_pos; bigZ_neg],
      uninterp_bigZ,
      true)
 
@@ -259,8 +268,8 @@ let uninterp_bigQ (AnyGlobConstr rc) =
 (* Actually declares the interpreter for bigQ *)
 let _ =
   Notation.declare_scope bigQ_scope;
-  Notation.declare_numeral_interpreter bigQ_scope
+  declare_numeral_interpreter "bignums.bigQ" bigQ_scope
     (bigQ_path, bigQ_module)
     interp_bigQ
-    ([DAst.make @@ GRef (bigQ_z, None)], uninterp_bigQ,
+    ([bigQ_z], uninterp_bigQ,
      true)