diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index d536be9bd..9b11e6879 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1139,15 +1139,16 @@ let interp c = match c with | VernacSyntax (whatfor,sel) -> vernac_syntax whatfor sel | VernacTacticGrammar al -> Metasyntax.add_tactic_grammar al | VernacGrammar (univ,al) -> vernac_grammar univ al - | VernacSyntaxExtension (s,l) -> vernac_syntax_extension s l + | VernacSyntaxExtension (local,s,l) -> vernac_syntax_extension local s l | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr | VernacOpenScope sc -> vernac_open_scope sc | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope qid scl - | VernacInfix (assoc,n,inf,qid,b,mv8,sc) -> - vernac_infix assoc n inf qid b mv8 sc - | VernacDistfix (assoc,n,inf,qid,sc) -> vernac_distfix assoc n inf qid sc - | VernacNotation (inf,c,pl,mv8,sc) -> - vernac_notation inf c pl mv8 sc + | VernacInfix (local,assoc,n,inf,qid,b,mv8,sc) -> + vernac_infix local assoc n inf qid b mv8 sc + | VernacDistfix (local,assoc,n,inf,qid,sc) -> + vernac_distfix local assoc n inf qid sc + | VernacNotation (local,inf,c,pl,mv8,sc) -> + vernac_notation local inf c pl mv8 sc (* Gallina *) | VernacDefinition (k,id,d,f,_) -> vernac_definition k id d f |