diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-06 00:27:16 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-06 00:27:16 +0000 |
| commit | e056138464f96fa493c47c1bc9f76e85fad9c262 (patch) | |
| tree | 05c71d7de9dc5dfbf77c115cf0b73c4336d0cda2 /parsing | |
| parent | 7cff0b6c6a492fd39640f7e73f4aa88f932fb0e2 (diff) | |
Ajout d'une commande pour afficher chaque coercion à la demande
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1333 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_basevernac.ml4 | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index a310bb15c..b4d380c80 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -173,13 +173,23 @@ GEXTEND Gram <:ast< (TEST_IMPLICIT_ARGS) >> (* Set printing of coercions *) + | "Set"; IDENT "Printing"; IDENT "Coercion"; + qidl = ne_qualidarg_list -> + <:ast< (PRINTING_COERCIONS_ON ($LIST qidl)) >> | "Set"; IDENT "Printing"; IDENT "Coercions" -> <:ast< (PRINTING_COERCIONS_ON) >> + | IDENT "Unset"; IDENT "Printing"; IDENT "Coercion"; + qidl = ne_qualidarg_list -> + <:ast< (PRINTING_COERCIONS_OFF ($LIST qidl)) >> | IDENT "Unset"; IDENT "Printing"; IDENT "Coercions" -> <:ast< (PRINTING_COERCIONS_OFF) >> + | IDENT "Test"; IDENT "Printing"; IDENT "Coercion"; + qidl = ne_qualidarg_list -> + <:ast< (TEST_PRINTING_COERCIONS ($LIST qidl)) >> | IDENT "Test"; IDENT "Printing"; IDENT "Coercions" -> <:ast< (TEST_PRINTING_COERCIONS) >> + (* Pour intervenir sur les tables de paramètres *) | "Set"; table = identarg; field = identarg; value = option_value -> |