diff options
| author | Maxime Dénès | 2019-05-24 16:35:09 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-05-24 16:35:09 +0200 |
| commit | 824b2393c9cc180c82dba00ee710124c24184945 (patch) | |
| tree | e0b4cea53f3994da70ccad490c86605074047d1d /plugins/syntax/numeral.ml | |
| parent | 46056cbe56f9c39fe3f8f5175aff9fd6427684b6 (diff) | |
Use global env in numeral and string notations
Since their introduction, these notations were incorrectly using the
proof-local environment.
Diffstat (limited to 'plugins/syntax/numeral.ml')
| -rw-r--r-- | plugins/syntax/numeral.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index ec8c2338fb..b0b6fa69bb 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -101,7 +101,9 @@ let type_error_of g ty = str " to Decimal.int or (option Decimal.int)." ++ fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int or Decimal.decimal could be used (you may need to require BinNums or Decimal or Int63 first).") -let vernac_numeral_notation env sigma local ty f g scope opts = +let vernac_numeral_notation local ty f g scope opts = + let env = Global.env () in + let sigma = Evd.from_env env in let dec_ty = locate_decimal () in let z_pos_ty = locate_z () in let int63_ty = locate_int63 () in |