diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-08 03:22:22 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-07 02:55:41 +0200 |
| commit | 1d0eb5d4d6fea88abc29798ee2004b2e27e952c6 (patch) | |
| tree | 24b4e369c4acbe2bb9c9ca79b84fc7ddff34e2d8 /grammar/compat5b.mlp | |
| parent | fee2365f13900b4d4f4b88c986cbbf94403eeefa (diff) | |
[camlpX] Remove camlp4 compat layer.
We remove the camlp4 compatibility layer, and try to clean up
most structures. `parsing/compat` is gone.
We added some documentation to the lexer/parser interfaces that are
often obscured by module includes.
Diffstat (limited to 'grammar/compat5b.mlp')
| -rw-r--r-- | grammar/compat5b.mlp | 23 |
1 files changed, 0 insertions, 23 deletions
diff --git a/grammar/compat5b.mlp b/grammar/compat5b.mlp deleted file mode 100644 index 46802a825..000000000 --- a/grammar/compat5b.mlp +++ /dev/null @@ -1,23 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** Adding a bit of camlp5 syntax to camlp4 for compatibility: - - EXTEND ... becomes EXTEND Gram ... -*) - -open Camlp4.PreCast - -let rec my_token_filter = parser - | [< '(KEYWORD "EXTEND",_ as t); s >] -> - [< 't; '(UIDENT "Gram", Loc.ghost); my_token_filter s >] - | [< 'tokloc; s >] -> [< 'tokloc; my_token_filter s >] - | [< >] -> [< >] - -let _ = - Token.Filter.define_filter (Gram.get_filter()) - (fun prev strm -> prev (my_token_filter strm)) |