diff options
Diffstat (limited to 'extraction/extraction.v')
| -rw-r--r-- | extraction/extraction.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index ffa06ddf..82b0a023 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -124,7 +124,7 @@ Extract Constant Cabs.cabsloc => byteno: int; ident : int; }". -Extract Constant Cabs.string => "String.t". +Extract Inlined Constant Cabs.string => "String.t". Extract Constant Cabs.char_code => "int64". (* Int31 *) |