Ajout des fonctions prpattern et prrawterm

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@184 85f007b7-540e-0410-9357-904b9bb8a0f7

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"