Updated version 8.9.0 from 'upstream/8.9.0'

with Debian dir 81a4f85bc45e59aa1eadb4797f0eb0b8039efb63

1 files changed, 15 insertions, 5 deletions

diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index acb297dd..53153198 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -28,7 +28,7 @@ let make_kn dir id = Globnames.encode_mind (make_dir dir) (Id.of_string id)
 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 ascii_module = ["Coq";"Strings";"Ascii"]
@@ -83,8 +83,18 @@ let make_ascii_string n =
 
 let uninterp_ascii_string (AnyGlobConstr r) = Option.map make_ascii_string (uninterp_ascii r)
 
+open Notation
+
+let at_declare_ml_module f x =
+  Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
+
 let _ =
-  Notation.declare_string_interpreter "char_scope"
-    (ascii_path,ascii_module)
-    interp_ascii_string
-    ([DAst.make @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true)
+  let sc = "char_scope" in
+  register_string_interpretation sc (interp_ascii_string,uninterp_ascii_string);
+  at_declare_ml_module enable_prim_token_interpretation
+    { pt_local = false;
+      pt_scope = sc;
+      pt_interp_info = Uid sc;
+      pt_required = (ascii_path,ascii_module);
+      pt_refs = [static_glob_Ascii];
+      pt_in_match = true }