diff options
| -rw-r--r-- | parsing/printer.ml | 18 | ||||
| -rw-r--r-- | parsing/printer.mli | 3 |
2 files changed, 21 insertions, 0 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index 9b20ea7443..e7d53dabb9 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -89,6 +89,7 @@ let rec gencompr k gt = in gpr gt + (* [at_top] means ids of env must be avoided in bound variables *) let gentermpr_core at_top k env t = let uenv = unitize_env env in @@ -127,6 +128,23 @@ let fprtype_env env typ = let fprtype = fprtype_env (gLOB nil_sign) +let genpatternpr k t = + try + gencompr k (Termast.ast_of_pattern t) + with Failure _ | Anomaly _ | UserError _ | Not_found -> + [< 'sTR"<PP error: non-printable term>" >];; + +let prpattern = genpatternpr CCI + +let genrawtermpr k env t = + let uenv = unitize_env env in + try + gencompr k (Termast.ast_of_rawconstr uenv t) + with Failure _ | Anomaly _ | UserError _ | Not_found -> + [< 'sTR"<PP error: non-printable term>" >];; + +let prrawterm = genrawtermpr CCI (gLOB nil_sign) + let gentacpr gt = let rec gpr gt = Esyntax.genprint "tactic" diff --git a/parsing/printer.mli b/parsing/printer.mli index a190b5e65e..96f282cace 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -22,6 +22,9 @@ val fterm0 : 'a assumptions -> constr -> std_ppcmds val term0 : 'a assumptions -> constr -> std_ppcmds val term0_at_top : 'a assumptions -> constr -> std_ppcmds +val prrawterm : Rawterm.rawconstr -> std_ppcmds +val prpattern : Rawterm.pattern -> std_ppcmds + val pr_sign : var_context -> std_ppcmds val pr_env_opt : context -> std_ppcmds |