diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/syntax/int63_syntax.ml | 1 | ||||
| -rw-r--r-- | plugins/syntax/numeral.ml | 2 | ||||
| -rw-r--r-- | plugins/syntax/string_notation.ml | 1 |
3 files changed, 3 insertions, 1 deletions
diff --git a/plugins/syntax/int63_syntax.ml b/plugins/syntax/int63_syntax.ml index 73a9341145..b14b02f3bb 100644 --- a/plugins/syntax/int63_syntax.ml +++ b/plugins/syntax/int63_syntax.ml @@ -43,6 +43,7 @@ let _ = let id_int63 = Nametab.locate q_id_int63 in let o = { to_kind = Int63, Direct; to_ty = id_int63; + to_post = [||]; of_kind = Int63, Direct; of_ty = id_int63; ty_name = q_int63; diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index 8635f39f1a..ad90a9a982 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -199,7 +199,7 @@ let vernac_number_notation local ty f g scope opts = | _, ((DecimalInt _ | DecimalUInt _ | Decimal _), _) -> warn_deprecated_decimal () | _ -> ()); - let o = { to_kind; to_ty; of_kind; of_ty; + let o = { to_kind; to_ty; to_post = [||]; of_kind; of_ty; ty_name = ty; warning = opts } in diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml index e7ed0d8061..dbb0e92d5c 100644 --- a/plugins/syntax/string_notation.ml +++ b/plugins/syntax/string_notation.ml @@ -82,6 +82,7 @@ let vernac_string_notation local ty f g scope = in let o = { to_kind = to_kind; to_ty = to_ty; + to_post = [||]; of_kind = of_kind; of_ty = of_ty; ty_name = ty; |