From 655eda6c576c2c8b52980144196a57fc7f9825ec Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 6 Dec 2001 02:02:15 +0000
Subject: Affichage des '_' pour Intros

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2276 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 syntax/PPTactic.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v
index a72a70ee57..3ca546f80d 100644
--- a/syntax/PPTactic.v
+++ b/syntax/PPTactic.v
@@ -370,6 +370,7 @@ Syntax tactic
   | intropatconj [<<(CONJPATTERN ($LIST $cp))>>] ->
                  [ "(" [<hov 0> (LISTCOMA ($LIST $cp))] ")" ]
   | intropatid [<<(IDENTIFIER ($VAR $id))>>] -> [ $id ]
+  | intropatwild [<<(WILDCAR)>>] -> [ "_" ]
 
 
   | patterncons [<<(NEPATTERNLIST $H ($LIST $T))>>]
-- 
cgit v1.2.3