From 0ee8d96df1357c69ae1d277caeca81a92b7e9bd4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 24 Jul 2000 13:45:10 +0000
Subject: Passage à des contextes de vars et de rels pouvant contenir des
 déclarations

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

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index a67f15e8eb..11e621acf7 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -32,11 +32,11 @@ let prid id = pP [< 'sTR(string_of_id id) >]
 
 let prconst (sp,j) =
     pP [< 'sTR"#"; 'sTR(string_of_path sp); 
-	  'sTR"="; term0 (gLOB nil_sign) j.uj_val >]
+	  'sTR"="; prterm j.uj_val >]
 
 let prvar ((id,a)) =
     pP [< 'sTR"#" ; 'sTR(string_of_id id) ; 'sTR":" ; 
-	  term0 (gLOB nil_sign) a >]
+	  prterm a >]
 
 let genprj f j =
   let (c,t) = Termast.with_casts f j in [< c; 'sTR " : "; t >]
@@ -56,7 +56,7 @@ let prglls glls = pP(pr_glls glls)
 
 let prctxt ctxt = pP(pr_ctxt ctxt)
 
-let pproof p = pP(print_proof Evd.empty nil_sign p)
+let pproof p = pP(print_proof Evd.empty empty_var_context p)
 
 let prevd evd = pP(pr_decls evd)
 
-- 
cgit v1.2.3