diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-20 23:33:19 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-20 23:33:19 +0000 |
| commit | 30aafbf07010a035ec8f033bde2cb183283d0371 (patch) | |
| tree | 68934fabae1a048302e184b79023e4d3e72e4d51 /parsing | |
| parent | e965f11f6cc8b08ef5683ae355c6b87f465bb076 (diff) | |
Rajout 'Set Printing Depth'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2039 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -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 0d527647b..b2b04a2d7 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 -> |