diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/astterm.ml | 11 | ||||
| -rw-r--r-- | parsing/lexer.mll | 4 |
2 files changed, 8 insertions, 7 deletions
diff --git a/parsing/astterm.ml b/parsing/astterm.ml index b595c901f8..7babfe020c 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -428,14 +428,15 @@ let globalize_ast ast = (* Installation of the AST quotations. "command" is used by default. *) -open Pcoq - let _ = - define_quotation true "command" (map_entry globalize_command Command.command) + Pcoq.define_quotation true "command" + (Pcoq.map_entry globalize_command Pcoq.Command.command) let _ = - define_quotation false "tactic" (map_entry globalize_ast Tactic.tactic) + Pcoq.define_quotation false "tactic" + (Pcoq.map_entry globalize_ast Pcoq.Tactic.tactic) let _ = - define_quotation false "vernac" (map_entry globalize_ast Vernac.vernac) + Pcoq.define_quotation false "vernac" + (Pcoq.map_entry globalize_ast Pcoq.Vernac.vernac) (*********************************************************************) diff --git a/parsing/lexer.mll b/parsing/lexer.mll index 5cb993b269..adafc2c842 100644 --- a/parsing/lexer.mll +++ b/parsing/lexer.mll @@ -84,7 +84,7 @@ let identchar = ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9'] let symbolchar = - ['!' '$' '%' '&' '*' '+' '-' '<' '>' '/' ':' '=' '?' '@' '^' '|' '~' '#'] + ['!' '$' '%' '&' '*' '+' '-' '<' '>' '/' ':' ';' '=' '?' '@' '^' '|' '~' '#'] let decimal_literal = ['0'-'9']+ let hex_literal = '0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']+ let oct_literal = '0' ['o' 'O'] ['0'-'7']+ @@ -98,7 +98,7 @@ rule token = parse if is_keyword s then ("",s) else ("IDENT",s) } | decimal_literal | hex_literal | oct_literal | bin_literal { ("INT", Lexing.lexeme lexbuf) } - | "(" | ")" | "[" | "]" | "{" | "}" | "<" | ">" | "." | "_" + | "(" | ")" | "[" | "]" | "{" | "}" | "." | "_" { ("", Lexing.lexeme lexbuf) } | symbolchar+ { ("", Lexing.lexeme lexbuf) } |