diff options
| author | Pierre Roux | 2020-09-03 13:11:00 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-11-04 20:14:47 +0100 |
| commit | dfcb15141a19db4f1cc61c14d1cdad0275009356 (patch) | |
| tree | 397fe74273788ff980fe564fa2e812cd004ff847 /plugins/syntax/numeral.ml | |
| parent | 3f04bd0a74575d93b2a5c1dfff2bd5a364bfac59 (diff) | |
[numeral notation] Add a pre/postprocessing
This will enable to define numeral notation on non inductive by using
an inductive type as proxy and those translations to translate to/from
the actual type to the inductive type.
Diffstat (limited to 'plugins/syntax/numeral.ml')
| -rw-r--r-- | plugins/syntax/numeral.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |