From c8a6a2b4e9bc7bd03c5022e4dc90de4029a4d7e5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 27 Nov 2000 10:26:41 +0000
Subject: Affichage des définitions locales

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@974 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/pretty.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 6aaffa19df..152e2a50ac 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -45,9 +45,10 @@ let print_impl_args = function
    synthesizes the type nat of the abstraction on u *)
 
 let print_named_def name body typ =
-  [< 'sTR "*** [" ; 'sTR name ; 'sPC; 
-     hOV 0 [< 'sTR "="; prterm body; 'sPC; 'sTR ": "; prtype typ >] ;
-     'sTR "]"; 'fNL >]
+  [< 'sTR "*** ["; 'sTR name ; 'sPC; 
+     hOV 0 [< 'sTR ":="; 'sPC; prterm body; 'sPC;
+	      'sTR ": "; prtype typ >];
+	   'sTR "]"; 'fNL >]
 
 let print_named_assum name typ =
   [< 'sTR "*** [" ; 'sTR name ; 'sTR " : "; prtype typ; 'sTR "]"; 'fNL >]
-- 
cgit v1.2.3