From 26712a2522e421fe2a6543fa7ab1a6f8ab1a2f44 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 16 Apr 2003 22:13:22 +0000
Subject: prettyprint des constr_substituted + un wrapping de prglobal pour
 qu'il n'echoue jamais lors d'un débug

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3928 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/include         |  1 +
 dev/top_printers.ml | 11 ++++++++++-
 2 files changed, 11 insertions(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/include b/dev/include
index 6b8470b302..eb370a5d84 100644
--- a/dev/include
+++ b/dev/include
@@ -12,6 +12,7 @@
 #install_printer  (* rawconstr *) pprawterm;;
 
 #install_printer  (* constr *) ppterm;;
+#install_printer  (* constr_substituted *) ppsterm;; 
 #install_printer  (* universe *)  print_uni;;
 #install_printer  (* universes *)  pp_universes;;
 #install_printer  (* type_judgement*) pptype;;
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 29cfe5c2a6..cf73540e5f 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -35,12 +35,21 @@ let prast c = pp(print_ast c)
 let prastpat c = pp(print_astpat c)
 let prastpatl c = pp(print_astlpat c)
 let ppterm x = pp(prterm x)
+let ppsterm x = ppterm (Declarations.force x)
 let ppterm_univ x = Constrextern.with_universes ppterm x
 let pprawterm = (fun x -> pp(pr_rawterm x))
 let pppattern = (fun x -> pp(pr_pattern x))
 let pptype = (fun x -> pp(prtype x))
 
-let prglobal = (fun x -> pp(pr_global x))
+let safe_prglobal = function 
+  | ConstRef kn -> pp (str "CONSTREF(" ++ pr_kn kn ++ str ")")
+  | IndRef (kn,i) -> pp (str "INDREF(" ++ pr_kn kn ++ str "," ++ 
+			  int i ++ str ")")
+  | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ pr_kn kn ++ str "," ++ 
+				      int i ++ str "," ++ int j ++ str ")")
+  | VarRef id -> pp (str "VARREF(" ++ pr_id id ++ str ")")
+
+let prglobal x = try pp(pr_global x) with _ -> safe_prglobal x
 
 let prid id = pp (pr_id id)
 let prlab l = pp (pr_lab l)
-- 
cgit v1.2.3