diff options
| author | delahaye | 2000-11-28 14:08:18 +0000 |
|---|---|---|
| committer | delahaye | 2000-11-28 14:08:18 +0000 |
| commit | 4800380437b6b133c7a9346aafa9c4e2b76527d7 (patch) | |
| tree | 447b2dfbd93d1e12dc7dcf47f5fd8f105d8d09a1 /parsing | |
| parent | 4c36f26e02e8c1df3f0851250526d89fd81d8448 (diff) | |
Elimination du '
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1000 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 18 | ||||
| -rw-r--r-- | parsing/lexer.mll | 8 |
2 files changed, 14 insertions, 12 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 66b016cfce..7cdf643980 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -54,7 +54,7 @@ GEXTEND Gram [ [ l = LIST1 qualidarg -> l ] ] ; ne_qualidconstarg_list: - [ [ l = LIST1 qualidconstarg -> l ] ] + [ [ l = LIST1 qualidarg -> l ] ] ; ne_num_list: [ [ n = numarg; l = ne_num_list -> n :: l | n = numarg -> [n] ] ] @@ -269,9 +269,9 @@ GEXTEND Gram -> <:ast< (MATCHCONTEXT ($LIST $mrl)) >> | IDENT "Match"; com = constrarg; IDENT "With"; mrl = match_list -> <:ast< (MATCH $com ($LIST $mrl)) >> - | "'("; te = tactic_expr; ")" -> te - | "'("; te = tactic_expr; tel=LIST1 tactic_expr; ")" -> - <:ast< (APP $te ($LIST tel)) >> + | "("; te = tactic_expr; ")" -> te + | "("; te = tactic_expr; tel=LIST1 tactic_expr; ")" -> + <:ast< (APP $te ($LIST tel)) >> | IDENT "First" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> <:ast<(FIRST ($LIST $l))>> | IDENT "Info"; tc = tactic_expr -> <:ast< (INFO $tc) >> @@ -293,11 +293,13 @@ GEXTEND Gram tactic_arg: [ [ "()" -> <:ast< (VOID) >> | n = pure_numarg -> n - | c = constrarg -> + | id = identarg -> id + | "'"; c = constrarg -> (match c with - | Coqast.Node(_,"COMMAND",[Coqast.Nvar(_,s)]) -> <:ast<($VAR $s)>> - | Coqast.Node(_,"COMMAND",[Coqast.Node(_,"QUALID",[Coqast.Nvar(_,s)])]) -> <:ast<($VAR $s)>> - |_ -> c) ] ] + | Coqast.Node(_,"COMMAND",[Coqast.Nvar(_,s)]) -> <:ast<($VAR $s)>> + | Coqast.Node(_,"COMMAND",[Coqast.Node(_,"QUALID", + [Coqast.Nvar(_,s)])]) -> <:ast<($VAR $s)>> + |_ -> c) ] ] ; simple_tactic: [ [ IDENT "Fix"; n = numarg -> <:ast< (Fix $n) >> diff --git a/parsing/lexer.mll b/parsing/lexer.mll index 6597231700..06531fb0f6 100644 --- a/parsing/lexer.mll +++ b/parsing/lexer.mll @@ -120,7 +120,7 @@ let identchar = ['A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9'] let symbolchar = ['!' '$' '%' '&' '*' '+' ',' '@' '^' '#'] -let extrachar = symbolchar | ['\\' '/' '-' '<' '>' '|' ':' '?' '=' '~'] +let extrachar = 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']+ @@ -136,8 +136,8 @@ rule token = parse if is_keyword s then ("",s) else ("IDENT",s) } | decimal_literal | hex_literal | oct_literal | bin_literal { ("INT", Lexing.lexeme lexbuf) } - | "(" | ")" | "[" | "]" | "{" | "}" | "." | "_" | ";"| "`" | "``" | "()" | "'(" - | "->" | "\\/" | "/\\" | "|-" | ":=" | "<->" | extrachar + | "(" | ")" | "[" | "]" | "{" | "}" | "." | "_" | ";"| "`" | "``" | "()" + | "->" | "\\/" | "/\\" | "|-" | ":=" | "<->" | '\'' | extrachar { ("", Lexing.lexeme lexbuf) } | "." blank { ("", ".") } @@ -153,7 +153,7 @@ rule token = parse "<-"(symbolchar | '\\' | '/' | '|' | '-' | '?' | ':' | '=' | '<' | '~')+ | '~' (symbolchar | '\\' | '/' | '|' | '-' | '>' | ':' | '=' | '<' )+ | ':' (symbolchar | '\\' | '/' | '|' | '-' | '>' | ':' | '=' | '<' )+ | - '>' | '?') extrachar* | "<-" + '\'' symbolchar+ | '>' | '?') extrachar* | "<-" { ("", Lexing.lexeme lexbuf) } | symbolchar+ extrachar* { ("", Lexing.lexeme lexbuf) } |