1 files changed, 19 insertions, 9 deletions

diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 372e8ff3..49497aef 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -30,7 +30,7 @@ let make_dir l = DirPath.make (List.rev_map Id.of_string l)
 let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
 let is_gr c gr = match DAst.get c with
-| GRef (r, _) -> Globnames.eq_gr r gr
+| GRef (r, _) -> GlobRef.equal r gr
 | _ -> false
 
 let positive_path = make_path binnums "positive"
@@ -66,7 +66,7 @@ let pos_of_bignat ?loc x =
 let rec bignat_of_pos c = match DAst.get c with
   | GApp (r, [a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a)
   | GApp (r, [a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a))
-  | GRef (a, _) when Globnames.eq_gr a glob_xH -> Bigint.one
+  | GRef (a, _) when GlobRef.equal a glob_xH -> Bigint.one
   | _ -> raise Non_closed_number
 
 (**********************************************************************)
@@ -98,7 +98,7 @@ let z_of_int ?loc n =
 let bigint_of_z c = match DAst.get c with
   | GApp (r,[a]) when is_gr r glob_POS -> bignat_of_pos a
   | GApp (r,[a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a)
-  | GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero
+  | GRef (a, _) when GlobRef.equal a glob_ZERO -> Bigint.zero
   | _ -> raise Non_closed_number
 
 (**********************************************************************)
@@ -131,9 +131,19 @@ let uninterp_r (AnyGlobConstr p) =
   with Non_closed_number ->
     None
 
-let _ = Notation.declare_numeral_interpreter "R_scope"
-  (r_path,["Coq";"Reals";"Rdefinitions"])
-  r_of_int
-  ([DAst.make @@ GRef (glob_IZR, None)],
-    uninterp_r,
-    false)
+open Notation
+
+let at_declare_ml_module f x =
+  Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
+
+let r_scope = "R_scope"
+
+let _ =
+  register_bignumeral_interpretation r_scope (r_of_int,uninterp_r);
+  at_declare_ml_module enable_prim_token_interpretation
+    { pt_local = false;
+      pt_scope = r_scope;
+      pt_interp_info = Uid r_scope;
+      pt_required = (r_path,["Coq";"Reals";"Rdefinitions"]);
+      pt_refs = [glob_IZR];
+      pt_in_match = false }