diff options
| -rw-r--r-- | parsing/g_basevernac.ml4 | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index 0d527647bb..b2b04a2d70 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -193,6 +193,11 @@ GEXTEND Gram | IDENT "Test"; IDENT "Implicit"; IDENT "Arguments" -> <:ast< (TEST_IMPLICIT_ARGS) >> + (* Set printing depth *) + (* An explicit entry, to be factorized with Printing Coercions *) + | "Set"; table = IDENT "Printing"; field = IDENT "Depth"; n = numarg -> + <:ast< (SetTableField ($VAR $table) ($VAR $field) $n) >> + (* Set printing of coercions *) | "Set"; IDENT "Printing"; IDENT "Coercion"; qidl = ne_qualidarg_list -> |