From e056138464f96fa493c47c1bc9f76e85fad9c262 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 6 Feb 2001 00:27:16 +0000
Subject: 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
---
 parsing/g_basevernac.ml4 | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index a310bb15c6..b4d380c804 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 ->
-- 
cgit v1.2.3