From 7099ced3316a9bd3f47a283ae224ca0bd29dcec9 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 7 Sep 1999 15:48:50 +0000
Subject: pretty-print A->B

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@46 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_minicoq.g4 | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/parsing/g_minicoq.g4 b/parsing/g_minicoq.g4
index ccf22ce448..7b7dca0ad4 100644
--- a/parsing/g_minicoq.g4
+++ b/parsing/g_minicoq.g4
@@ -145,6 +145,8 @@ let rec pp bv = function
   | DOP0 (Sort (Type u)) -> print_type u
   | DOP2 (Lambda, t, DLAM(na, c)) ->
       [< 'sTR"["; print_name na; 'sTR":"; pp bv t; 'sTR"]"; pp (na::bv) c >]
+  | DOP2 (Prod, t, DLAM(Anonymous, c)) ->
+      [< pp bv t; 'sTR"->"; pp (Anonymous::bv) c >]
   | DOP2 (Prod, t, DLAM(na, c)) ->
       [< 'sTR"("; print_name na; 'sTR":"; pp bv t; 'sTR")"; pp (na::bv) c >]
   | DOP2 (Cast, c, t) ->
-- 
cgit v1.2.3