diff options
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
| -rw-r--r-- | plugins/syntax/string_syntax.ml | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index c22869f4d6..ca1bf0df27 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -64,10 +64,17 @@ let uninterp_string (AnyGlobConstr r) = with Non_closed_string -> None +open Notation + +let at_declare_ml_module f x = + Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name + let _ = - Notation.declare_string_interpreter "string_scope" - (string_path,["Coq";"Strings";"String"]) - interp_string - ([DAst.make @@ GRef (static_glob_String,None); - DAst.make @@ GRef (static_glob_EmptyString,None)], - uninterp_string, true) + let sc = "string_scope" in + register_string_interpretation sc (interp_string,uninterp_string); + at_declare_ml_module enable_prim_token_interpretation + { pt_scope = sc; + pt_uid = sc; + pt_required = (string_path,["Coq";"Strings";"String"]); + pt_refs = [static_glob_String; static_glob_EmptyString]; + pt_in_match = true } |