From 5139432d6087f49ef549d8375a1a61db56f86dd1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 1 Jun 2000 20:44:16 +0000
Subject: Mise en place d'un choix constr/typed_type en remplacement de
 certains Cast

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@484 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/top_printers.ml | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 35cd38acbd..a67f15e8eb 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -38,13 +38,10 @@ let prvar ((id,a)) =
     pP [< 'sTR"#" ; 'sTR(string_of_id id) ; 'sTR":" ; 
 	  term0 (gLOB nil_sign) a >]
 
-let genprj f j = [< (f (gLOB nil_sign)j.uj_val); 
-                 'sTR " : ";
-               (f (gLOB nil_sign)j.uj_type);
-                  'sTR " : ";
-               (f  (gLOB nil_sign)j.uj_kind)>]
+let genprj f j =
+  let (c,t) = Termast.with_casts f j in [< c; 'sTR " : "; t >]
 
-let prj j = pP (genprj term0 j)
+let prj j = pP (genprj prjudge j)
 
 
 let prsp sp = pP[< 'sTR(string_of_path sp) >]
-- 
cgit v1.2.3