Généralisation du type ltac Identifier en IntroPattern; prise en compte des IntroPattern au parsing, à l'interprétation, à la traduction

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

1 files changed, 1 insertions, 14 deletions

diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index d663c942ac..5704d853be 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -207,19 +207,6 @@ let pr_with_constr prc = function
   | None -> mt ()
   | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c)
 
-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
   | [] -> mt ()
   | ids -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_case_intro_pattern ids)
@@ -765,7 +752,7 @@ and pr_tacarg env = function
   | TacDynamic (loc,t) ->
       pr_with_comments loc (str ("<dynamic ["^(Dyn.tag t)^"]>"))
   | MetaIdArg (loc,s) -> pr_with_comments loc (str ("$" ^ s))
-  | Identifier id -> pr_id id
+  | IntroPattern ipat -> str "ipattern:" ++ pr_intro_pattern ipat
   | TacVoid -> str "()"
   | Reference r -> pr_ref r
   | ConstrMayEval c ->