diff options
Diffstat (limited to 'plugins/syntax/g_string.mlg')
| -rw-r--r-- | plugins/syntax/g_string.mlg | 21 |
1 files changed, 3 insertions, 18 deletions
diff --git a/plugins/syntax/g_string.mlg b/plugins/syntax/g_string.mlg index cc8c13a84b..c94119fdb0 100644 --- a/plugins/syntax/g_string.mlg +++ b/plugins/syntax/g_string.mlg @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -19,22 +19,7 @@ open Stdarg } VERNAC COMMAND EXTEND StringNotation CLASSIFIED AS SIDEFF - | #[ locality = Attributes.locality; ] ![proof] [ "String" "Notation" reference(ty) reference(f) reference(g) ":" + | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) ":" ident(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 } + { vernac_string_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) } END |