diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /plugins/syntax/ascii_syntax.ml | |
parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) |
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'plugins/syntax/ascii_syntax.ml')
-rw-r--r-- | plugins/syntax/ascii_syntax.ml | 20 |
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 } |