diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 5 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 7 |
2 files changed, 7 insertions, 5 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index cb7507d9c1..3baed8992d 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -538,9 +538,10 @@ GEXTEND Gram in VernacInstance (not (use_non_locality ()), sup, (n, expl, t), props, pri) - | IDENT "Existing"; IDENT "Instance"; is = identref -> VernacDeclareInstance is + | IDENT "Existing"; IDENT "Instance"; is = global -> + VernacDeclareInstance (not (use_section_locality ()), is) - | IDENT "Existing"; IDENT "Class"; is = identref -> VernacDeclareClass is + | IDENT "Existing"; IDENT "Class"; is = global -> VernacDeclareClass is (* Implicit *) | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global; diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 3ef45072cc..873558dff9 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -736,11 +736,12 @@ let rec pr_vernac = function pr_and_type_binders_arg l ++ spc () ++ str "]") - | VernacDeclareInstance id -> - hov 1 (str"Existing" ++ spc () ++ str"Instance" ++ spc () ++ pr_lident id) + | VernacDeclareInstance (glob, id) -> + hov 1 (pr_non_locality (not glob) ++ + str"Existing" ++ spc () ++ str"Instance" ++ spc () ++ pr_reference id) | VernacDeclareClass id -> - hov 1 (str"Existing" ++ spc () ++ str"Class" ++ spc () ++ pr_lident id) + hov 1 (str"Existing" ++ spc () ++ str"Class" ++ spc () ++ pr_reference id) (* Modules and Module Types *) | VernacDefineModule (export,m,bl,tys,bd) -> |