diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-03 16:23:22 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-03 16:23:22 +0000 |
| commit | 4a2b9073e61de1ab000b26652d94e63b382ce7d2 (patch) | |
| tree | 73b7d5f031de7fb58f639fc3a974bb5bbafa4347 /parsing | |
| parent | 64dfc220b6307c867078ee5a860e92604f6df694 (diff) | |
bug make_strength repare
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@200 85f007b7-540e-0410-9357-904b9bb8a0f7
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 b595c901f..7babfe020 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 5cb993b26..adafc2c84 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) } |