diff options
| author |  Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
| commit | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (patch) | |
| tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /parsing/printer.mli | |
| parent | bf12eb93f3f6a6a824a10878878fadd59745aae0 (diff) | |
Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg
Diffstat (limited to 'parsing/printer.mli')
| -rw-r--r-- | parsing/printer.mli | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/parsing/printer.mli b/parsing/printer.mli index a034f0ed..3abe90e7 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -31,6 +31,17 @@ val pr_lconstr : constr -> std_ppcmds val pr_constr_env : env -> constr -> std_ppcmds val pr_constr : constr -> std_ppcmds +(** Same, but resilient to [Nametab] errors. Prints fully-qualified + names when [shortest_qualid_of_global] has failed. Prints "??" + in case of remaining issues (such as reference not in env). *) + +val safe_pr_lconstr_env : env -> constr -> std_ppcmds +val safe_pr_lconstr : constr -> std_ppcmds + +val safe_pr_constr_env : env -> constr -> std_ppcmds +val safe_pr_constr : constr -> std_ppcmds + + val pr_open_constr_env : env -> open_constr -> std_ppcmds val pr_open_constr : open_constr -> std_ppcmds |