diff options
| author | Hugo Herbelin | 2020-08-29 23:11:01 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-10 22:34:24 +0200 |
| commit | 0d11cdd7fe6605666a274168e40acb11e1b05ab6 (patch) | |
| tree | 90e17d3af1902c96b3d49078dd5ead860c7b46ce | |
| parent | 03d55f990bb7a2c4f5c1fefa408b94a8a93e8d05 (diff) | |
Print Scope & cie: Add parentheses around notation interpretation.
This is to be consistent with the use of parentheses in the syntax of
Notation and to support a list of attribute afterwards.
| -rw-r--r-- | vernac/vernacentries.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index fe27d9ac8a..0d3f38d139 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1790,11 +1790,11 @@ let vernac_print ~pstate = | PrintHintDbName s -> Hints.pr_hint_db_by_name env sigma s | PrintHintDb -> Hints.pr_searchtable env sigma | PrintScopes -> - Notation.pr_scopes (Constrextern.without_symbols (pr_lglob_constr_env env)) + Notation.pr_scopes (Constrextern.without_symbols (pr_glob_constr_env env)) | PrintScope s -> - Notation.pr_scope (Constrextern.without_symbols (pr_lglob_constr_env env)) s + Notation.pr_scope (Constrextern.without_symbols (pr_glob_constr_env env)) s | PrintVisibility s -> - Notation.pr_visibility (Constrextern.without_symbols (pr_lglob_constr_env env)) s + Notation.pr_visibility (Constrextern.without_symbols (pr_glob_constr_env env)) s | PrintAbout (ref_or_by_not,udecl,glnumopt) -> print_about_hyp_globs ~pstate ref_or_by_not udecl glnumopt | PrintImplicit qid -> @@ -1830,7 +1830,7 @@ let vernac_locate ~pstate = let open Constrexpr in function | LocateTerm {v=ByNotation (ntn, sc)} -> let _, env = get_current_or_global_context ~pstate in Notation.locate_notation - (Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc + (Constrextern.without_symbols (pr_glob_constr_env env)) ntn sc | LocateLibrary qid -> print_located_library qid | LocateModule qid -> Prettyp.print_located_module qid | LocateOther (s, qid) -> Prettyp.print_located_other s qid |