diff options
| -rw-r--r-- | parsing/pcoq.ml4 | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index f9cd0839fe..951a576c8f 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -397,6 +397,13 @@ let define_quotation default s e = ast: [ [ "<<"; c = e; ">>" -> c ] ]; END); (GEXTEND Gram + GLOBAL: ast; ast: - [ [ "<"; ":"; IDENT $s$; ":"; "<"; c = e; ">>" -> c ] ]; + [ [ _ = langle_colon; IDENT $s$; _ = colon_langle; c = e; ">>" -> c ] ]; + langle_colon: + [ [ "<"; ":" -> () + | "<:" -> () ] ]; (* Maximal token rule *) + colon_langle: + [ [ ":"; "<" -> () + | ":<" -> () ] ]; (* Maximal token rule *) END) |