diff options
Diffstat (limited to 'plugins/syntax')
| -rw-r--r-- | plugins/syntax/g_numeral.mlg | 21 | ||||
| -rw-r--r-- | plugins/syntax/g_string.mlg | 20 |
2 files changed, 35 insertions, 6 deletions
diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg index 73a2b99434..baa4ae0306 100644 --- a/plugins/syntax/g_numeral.mlg +++ b/plugins/syntax/g_numeral.mlg @@ -35,8 +35,23 @@ ARGUMENT EXTEND numnotoption END VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF - | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" + | #[ locality = Attributes.locality; ] ![proof][ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" ident(sc) numnotoption(o) ] -> - { let (sigma, env) = Pfedit.get_current_context () in - vernac_numeral_notation env sigma (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } + + { (* It is a bug to use the proof context here, but at the request of + * the reviewers we keep this broken behavior for now. The Global env + * should be used instead, and the `env, sigma` parameteter to the + * numeral notation command removed. + *) + fun ~pstate -> + let sigma, env = match pstate with + | None -> + let env = Global.env () in + let sigma = Evd.from_env env in + sigma, env + | Some pstate -> + Pfedit.get_current_context pstate + in + vernac_numeral_notation env sigma (Locality.make_module_locality locality) ty f g (Id.to_string sc) o; + pstate } END diff --git a/plugins/syntax/g_string.mlg b/plugins/syntax/g_string.mlg index 171e0e213d..cc8c13a84b 100644 --- a/plugins/syntax/g_string.mlg +++ b/plugins/syntax/g_string.mlg @@ -19,8 +19,22 @@ open Stdarg } VERNAC COMMAND EXTEND StringNotation CLASSIFIED AS SIDEFF - | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) ":" + | #[ locality = Attributes.locality; ] ![proof] [ "String" "Notation" reference(ty) reference(f) reference(g) ":" ident(sc) ] -> - { let (sigma, env) = Pfedit.get_current_context () in - vernac_string_notation env sigma (Locality.make_module_locality locality) ty f g (Id.to_string sc) } + { (* It is a bug to use the proof context here, but at the request of + * the reviewers we keep this broken behavior for now. The Global env + * should be used instead, and the `env, sigma` parameteter to the + * numeral notation command removed. + *) + fun ~pstate -> + let sigma, env = match pstate with + | None -> + let env = Global.env () in + let sigma = Evd.from_env env in + sigma, env + | Some pstate -> + Pfedit.get_current_context pstate + in + vernac_string_notation env sigma (Locality.make_module_locality locality) ty f g (Id.to_string sc); + pstate } END |