From 4e4e62ccb7c0dc2dc2796e32cfab5b80d268ccf8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 30 Apr 2000 00:44:47 +0000
Subject: Bug affichage Error et Value

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@388 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/SpecifSyntax.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v
index c399a74eb3..8b467fe13f 100644
--- a/theories/Init/SpecifSyntax.v
+++ b/theories/Init/SpecifSyntax.v
@@ -121,5 +121,5 @@ Syntax constr
     Except_imp [<<(except $1 $t2)>>] -> [ [<hov 0> "Except " $t2 ] ]
 
 (* Pretty-printing of [error] and [value] *)
-  | Error_imp [<<(error $1 $t2)>>] -> [ [<hov 0> "Error " $t2 ] ]
-  | Value_imp [<<(value $1 $t2)>>] -> [ [<hov 0> "Value " $t2 ] ].
+  | Error_imp [<<(error $t1)>>]     -> [ [<hov 0> "Error" ] ]
+  | Value_imp [<<(value $t1 $t2)>>] -> [ [<hov 0> "(Value " $t2 ")" ] ].
-- 
cgit v1.2.3