Retablissement pour le traducteur d'une copie de pr_intro_pattern base sur la copie traduisante de pr_id

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

1 files changed, 13 insertions, 0 deletions

diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index cbe659063..9274fba05 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -207,6 +207,19 @@ let pr_with_constr prc = function
   | None -> mt ()
   | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c)
 
+(* Translator copy of pr_intro_pattern based on a translating "pr_id" *)
+let rec pr_intro_pattern = function
+  | IntroOrAndPattern pll -> pr_case_intro_pattern pll
+  | IntroWildcard -> str "_"
+  | IntroIdentifier id -> pr_id id
+and pr_case_intro_pattern = function
+  | [_::_ as pl] ->
+      str "(" ++ hv 0 (prlist_with_sep pr_coma pr_intro_pattern pl) ++ str ")"
+  | pll ->
+      str "[" ++
+      hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
+      ++ str "]"
+
 let pr_with_names = function
   | None -> mt ()
   | Some ipat -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)