diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 44e7cbad7..4c24f3505 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -284,8 +284,8 @@ let vernac_bind_scope sc cll = let vernac_open_close_scope = Notation.open_close_scope -let vernac_arguments_scope qid scl = - Notation.declare_arguments_scope (global qid) scl +let vernac_arguments_scope local qid scl = + Notation.declare_arguments_scope local (global qid) scl let vernac_infix = Metasyntax.add_infix @@ -666,9 +666,11 @@ let vernac_hints = Auto.add_hints let vernac_syntactic_definition = Command.syntax_definition -let vernac_declare_implicits locqid = function - | Some imps -> Impargs.declare_manual_implicits (Nametab.global locqid) imps - | None -> Impargs.declare_implicits (Nametab.global locqid) +let vernac_declare_implicits local locqid = function + | Some imps -> + Impargs.declare_manual_implicits local (Nametab.global locqid) imps + | None -> + Impargs.declare_implicits local (Nametab.global locqid) let vernac_reserve idl c = let t = Constrintern.interp_type Evd.empty (Global.env()) c in @@ -1122,7 +1124,7 @@ let interp c = match c with | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl | VernacOpenCloseScope sc -> vernac_open_close_scope sc - | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope qid scl + | VernacArgumentsScope (lcl,qid,scl) -> vernac_arguments_scope lcl qid scl | VernacInfix (local,mv,qid,sc) -> vernac_infix local mv qid sc | VernacNotation (local,c,infpl,sc) -> vernac_notation local c infpl sc @@ -1193,7 +1195,7 @@ let interp c = match c with | VernacDeclareTacticDefinition (x,l) -> vernac_declare_tactic_definition x l | VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints | VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b - | VernacDeclareImplicits (qid,l) -> vernac_declare_implicits qid l + | VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l | VernacReserve (idl,c) -> vernac_reserve idl c | VernacSetOpacity (opaq, qidl) -> List.iter (vernac_set_opacity opaq) qidl | VernacSetOption (key,v) -> vernac_set_option key v |