diff options
Diffstat (limited to 'parsing/printer.ml')
| -rw-r--r-- | parsing/printer.ml | 18 |
1 files changed, 18 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" |