From 2db7263c70fbf401422fe4797e86659c4d7c4310 Mon Sep 17 00:00:00 2001
From: coq
Date: Fri, 15 Jul 2005 17:13:11 +0000
Subject: Add some debug printing functions.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7236 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/printer.ml  | 8 ++++++++
 parsing/printer.mli | 2 ++
 2 files changed, 10 insertions(+)

diff --git a/parsing/printer.ml b/parsing/printer.ml
index 5f6612e3a6..0677f2699f 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -189,6 +189,11 @@ let pr_named_context_of env =
 	  (fun env d pps -> pps ++ ws 2 ++ pr_var_decl env d)
           env ~init:(mt ()))
 
+let pr_named_context env ne_context = 
+  hv 0 (Sign.fold_named_context
+	  (fun d pps -> pps ++ ws 2 ++ pr_var_decl env d)
+          ne_context ~init:(mt ()))
+
 let pr_rel_context env rel_context =
   let rec prec env = function
     | [] -> (mt ()) 
@@ -205,6 +210,9 @@ let pr_rel_context env rel_context =
   in 
   hov 0 (prec env (List.rev rel_context))
 
+let pr_rel_context_of env =
+  pr_rel_context env (rel_context env)
+
 (* Prints an env (variables and de Bruijn). Separator: newline *)
 let pr_context_unlimited env =
   let sign_env =
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 8be938f815..4890b1bea2 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -51,8 +51,10 @@ val pr_ne_context_of : std_ppcmds -> env -> std_ppcmds
 val pr_var_decl     : env -> named_declaration -> std_ppcmds
 val pr_rel_decl     : env -> rel_declaration -> std_ppcmds
 
+val pr_named_context : env -> named_context -> std_ppcmds
 val pr_named_context_of : env -> std_ppcmds
 val pr_rel_context  : env -> rel_context -> std_ppcmds
+val pr_rel_context_of  : env -> std_ppcmds
 val pr_context_of   : env -> std_ppcmds
 
 val emacs_str       : string -> string
-- 
cgit v1.2.3