# Using string\_scope without Import-ing String

**URL:** <https://discourse.rocq-prover.org/t/using-string-scope-without-import-ing-string/390>\
**Category:** Using Rocq\
**Created:** [August 12, 2019, 4:00pm UTC](https://discourse.rocq-prover.org/t/using-string-scope-without-import-ing-string/390 "2019-08-12T16:00:30Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![ligvor](https://avatars.discourse-cdn.com/v4/letter/l/41988e/32.png) [@ligvor](https://discourse.rocq-prover.org/u/ligvor)\
**Post date:** [August 12, 2019, 4:00pm UTC](https://discourse.rocq-prover.org/t/using-string-scope-without-import-ing-string/390/1 "2019-08-12T16:00:30Z")

</div>

With 8.8.2 the code below compiles successfuly, but from 8.9 it fails with “Error: No interpretation for string “a”.”:

```
Require String.

Definition f (x : String.string) := tt.
Arguments f _%string_scope.

Check f "a".

```

I tried to modernize it, but could not get it to compile (without import String which messes with List.++)

```
Require String.

Delimit Scope string_scope with lstring.
Bind Scope string_scope with String.string.

Definition f (x : String.string) := tt.
(*Arguments f _%string_scope.*)
Arguments f _%lstring.

Check f "a".
```

---

<div class="post-metadata">

**Author:** ![Vincent](https://avatars.discourse-cdn.com/v4/letter/v/e9bcb4/32.png) [@Vincent](https://discourse.rocq-prover.org/u/Vincent)\
**Post date:** [August 13, 2019, 12:59pm UTC](https://discourse.rocq-prover.org/t/using-string-scope-without-import-ing-string/390/2 "2019-08-13T12:59:51Z")

</div>

Starting from Coq 8.9, you can import the StringSyntax module:

> Require String.  
> Import String.StringSyntax.

---

<div class="post-metadata">

**Author:** ![ligvor](https://avatars.discourse-cdn.com/v4/letter/l/41988e/32.png) [@ligvor](https://discourse.rocq-prover.org/u/ligvor)\
**Post date:** [August 13, 2019, 8:00pm UTC](https://discourse.rocq-prover.org/t/using-string-scope-without-import-ing-string/390/3 "2019-08-13T20:00:09Z")

</div>

Thank you Vincent! (8.9.0 does not work, but 8.9.1 does.)

Should have seen it here:  
[https://coq.github.io/doc/v8.10/refman/changes.html#details-of-changes-in-8-9-beta1](https://coq.github.io/doc/v8.10/refman/changes.html#details-of-changes-in-8-9-beta1)