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/string_notation.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/string_notation.ml')
| -rw-r--r-- | plugins/syntax/string_notation.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml index 5fae696d58..4234cee1bd 100644 --- a/plugins/syntax/string_notation.ml +++ b/plugins/syntax/string_notation.ml @@ -47,7 +47,9 @@ let type_error_of g ty = (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++ str " to Byte.byte or (option Byte.byte) or (list Byte.byte) or (option (list Byte.byte)).") -let vernac_string_notation env sigma local ty f g scope = +let vernac_string_notation local ty f g scope = + let env = Global.env () in + let sigma = Evd.from_env env in let app x y = mkAppC (x,[y]) in let cref q = mkRefC q in let cbyte = cref (q_byte ()) in |