From 5361cc1ac8baec7b519288dae36e9503d82d7709 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 5 Mar 2004 18:22:13 +0000
Subject: 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
---
 translate/pptacticnew.ml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index cbe6590633..9274fba051 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)
-- 
cgit v1.2.3