diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-01 23:06:29 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-01 23:06:29 +0000 |
| commit | 3a49dbf016e1ebf8f8d12ed43fde14c5619ca55e (patch) | |
| tree | 58b1f1b8956d88b8d56c497bbfdebc8387fc91c8 /parsing | |
| parent | 91448aa09ff9abbacef4e3328e87c049aa2d96eb (diff) | |
Ajout des fonctions prpattern et prrawterm
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@184 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -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 9b20ea744..e7d53dabb 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 a190b5e65..96f282cac 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 |