From ba18968685be05d370bb0a82fc3f5e403cdced9f Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 21 Jul 2000 17:31:35 +0000
Subject: retablissement minicoq (pour Jacek)

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

(limited to 'parsing')

diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4
index bf75cdd381..c14c5d0344 100644
--- a/parsing/g_minicoq.ml4
+++ b/parsing/g_minicoq.ml4
@@ -176,4 +176,5 @@ let rec pp bv = function
   | Rel n -> print_rel bv n
   | _ -> [< 'sTR"<???>" >]
 
-let pr_term _ ctx = pp (List.map fst (get_rels ctx))
+let pr_term _ ctx = pp (it_dbenv (fun l n _ -> n::l) [] ctx)
+
-- 
cgit v1.2.3