diff options
| author | Pierre-Marie Pédrot | 2019-05-27 10:11:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-27 10:11:20 +0200 |
| commit | 0f23bf68fd5e7adb9bd0bf5be7912061813348aa (patch) | |
| tree | 7e9fff16202c0585dc44d2e5fe6a92d7a35ce505 /plugins/syntax/string_notation.ml | |
| parent | 4e324a95217bedae198360d1078e3b664fb2deea (diff) | |
| parent | 824b2393c9cc180c82dba00ee710124c24184945 (diff) | |
Merge PR #10237: Fix some incorrect uses of proof-local environment
Reviewed-by: gares
Reviewed-by: ppedrot
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 |