aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/string_notation.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/syntax/string_notation.ml')
-rw-r--r--plugins/syntax/string_notation.ml11
1 files changed, 6 insertions, 5 deletions
diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml
index fff8e928c3..12ee4c6eda 100644
--- a/plugins/syntax/string_notation.ml
+++ b/plugins/syntax/string_notation.ml
@@ -80,11 +80,12 @@ let vernac_string_notation local ty f g scope =
else if has_type g (arrow cty (opt cbyte)) then Byte, Option
else type_error_of g ty
in
- let o = { sto_kind = to_kind;
- sto_ty = to_ty;
- sof_kind = of_kind;
- sof_ty = of_ty;
- string_ty = ty }
+ let o = { to_kind = to_kind;
+ to_ty = to_ty;
+ of_kind = of_kind;
+ of_ty = of_ty;
+ ty_name = ty;
+ warning = () }
in
let i =
{ pt_local = local;