diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-16 22:13:22 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-16 22:13:22 +0000 |
| commit | 26712a2522e421fe2a6543fa7ab1a6f8ab1a2f44 (patch) | |
| tree | 44392c4e0100954dba08befad5eb3c9e92a2d56e | |
| parent | e94f8b40f52e3c25c431082af80fc522cdfa098d (diff) | |
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
| -rw-r--r-- | dev/include | 1 | ||||
| -rw-r--r-- | dev/top_printers.ml | 11 |
2 files changed, 11 insertions, 1 deletions
diff --git a/dev/include b/dev/include index 6b8470b30..eb370a5d8 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 29cfe5c2a..cf73540e5 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) |