diff options
| -rw-r--r-- | API/API.mli | 2 | ||||
| -rw-r--r-- | intf/vernacexpr.ml | 2 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 5 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 9 |
5 files changed, 10 insertions, 10 deletions
diff --git a/API/API.mli b/API/API.mli index d1774afe5..3b2dc5a67 100644 --- a/API/API.mli +++ b/API/API.mli @@ -3799,7 +3799,7 @@ sig | VernacTimeout of int * vernac_expr | VernacFail of vernac_expr | VernacSyntaxExtension of - obsolete_locality * (lstring * syntax_modifier list) + bool * obsolete_locality * (lstring * syntax_modifier list) | VernacOpenCloseScope of obsolete_locality * (bool * scope_name) | VernacDelimiters of scope_name * string option | VernacBindScope of scope_name * class_rawexpr list diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 2adf522b7..8b6abb6e8 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -325,7 +325,7 @@ type vernac_expr = (* Syntax *) | VernacSyntaxExtension of - obsolete_locality * (lstring * syntax_modifier list) + bool * obsolete_locality * (lstring * syntax_modifier list) | VernacOpenCloseScope of obsolete_locality * (bool * scope_name) | VernacDelimiters of scope_name * string option | VernacBindScope of scope_name * class_rawexpr list diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b9a162bec..7a7746cc9 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -1134,14 +1134,13 @@ GEXTEND Gram | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring; l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] -> - Metasyntax.check_infix_modifiers l; let (loc,s) = s in - VernacSyntaxExtension (false,((loc,"x '"^s^"' y"),l)) + VernacSyntaxExtension (true, false,((loc,"x '"^s^"' y"),l)) | IDENT "Reserved"; IDENT "Notation"; local = obsolete_locality; s = ne_lstring; l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] - -> VernacSyntaxExtension (local,(s,l)) + -> VernacSyntaxExtension (false, local,(s,l)) (* "Print" "Grammar" should be here but is in "command" entry in order to factorize with other "Print"-based vernac entries *) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 4c50c2f36..b2ffdb25c 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -656,7 +656,7 @@ open Decl_kinds | None -> mt() | Some sc -> str" :" ++ spc() ++ str sc)) ) - | VernacSyntaxExtension (_,(s,l)) -> + | VernacSyntaxExtension (_, _,(s,l)) -> return ( keyword "Reserved Notation" ++ spc() ++ pr_located qs s ++ pr_syntax_modifiers l diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 8738e58e8..8322958f7 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -409,9 +409,10 @@ let dump_global r = (**********) (* Syntax *) -let vernac_syntax_extension locality local = +let vernac_syntax_extension locality local infix l = let local = enforce_module_locality locality local in - Metasyntax.add_syntax_extension local + if infix then Metasyntax.check_infix_modifiers (snd l); + Metasyntax.add_syntax_extension local l let vernac_delimiters sc = function | Some lr -> Metasyntax.add_delimiters sc lr @@ -1950,8 +1951,8 @@ let interp ?proof ?loc locality poly c = | VernacLocal _ -> assert false (* Syntax *) - | VernacSyntaxExtension (local,sl) -> - vernac_syntax_extension locality local sl + | VernacSyntaxExtension (infix, local,sl) -> + vernac_syntax_extension locality local infix sl | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl | VernacOpenCloseScope (local, s) -> vernac_open_close_scope locality local s |