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/g_numeral.mlg | |
| 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/g_numeral.mlg')
| -rw-r--r-- | plugins/syntax/g_numeral.mlg | 19 |
1 files changed, 2 insertions, 17 deletions
diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg index 0f0f3953da..5808385723 100644 --- a/plugins/syntax/g_numeral.mlg +++ b/plugins/syntax/g_numeral.mlg @@ -34,23 +34,8 @@ VERNAC ARGUMENT EXTEND numnotoption END VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF - | #[ locality = Attributes.locality; ] ![proof][ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" + | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" ident(sc) numnotoption(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 } + { vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } END |