Utilisation de intro_pattern dans NewDestruct/NewInduction

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

1 files changed, 6 insertions, 7 deletions

diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 6f56a72b27..2bbb2d0821 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -65,21 +65,20 @@ let pr_bindings prlc prc = pr_bindings_gen false prlc prc
 
 let pr_with_bindings prlc prc (c,bl) = prc c ++ pr_bindings prlc prc bl
 
-let pr_with_names = function
-  | [] -> mt ()
-  | ids -> spc () ++ str "as [" ++
-      hv 0 (prlist_with_sep (fun () -> spc () ++ str "| ")
-              (prlist_with_sep spc pr_id) ids ++ str "]")
-
 let rec pr_intro_pattern = function
   | IntroOrAndPattern pll ->
       str "[" ++
       hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
       ++ str "]"
-
   | IntroWildcard -> str "_"
   | IntroIdentifier id -> pr_id id
 
+let pr_with_names = function
+  | [] -> mt ()
+  | ids -> spc () ++ str "as [" ++
+      hv 0 (prlist_with_sep (fun () -> spc () ++ str "| ")
+              (prlist_with_sep spc pr_intro_pattern) ids ++ str "]")
+
 let pr_hyp_location pr_id = function
   | InHyp id -> spc () ++ pr_id id
   | InHypType id -> spc () ++ str "(type of " ++ pr_id id ++ str ")"