diff options
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
| -rw-r--r-- | plugins/syntax/string_syntax.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index ac17492d2..7474a8b0e 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -64,6 +64,6 @@ let _ = Notation.declare_string_interpreter "string_scope" (string_path,["Coq";"Strings";"String"]) interp_string - ([GRef (dummy_loc,static_glob_String); - GRef (dummy_loc,static_glob_EmptyString)], + ([GRef (Loc.ghost,static_glob_String); + GRef (Loc.ghost,static_glob_EmptyString)], uninterp_string, true) |