Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq

choisir un nom; utilisation de IntroAnonymous au lieu de None dans
l'argument "with_names" des tactiques induction, inversion et assert.


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

4 files changed, 12 insertions, 26 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index f7c05c7786..4f10bca748 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -176,6 +176,7 @@ GEXTEND Gram
       | "("; tc = LIST0 simple_intropattern SEP "," ; ")" -> IntroOrAndPattern [tc]
       | "()" -> IntroOrAndPattern [[]]
       | "_" -> IntroWildcard
+      | "?" -> IntroAnonymous
       | id = ident -> IntroIdentifier id
       ] ]
   ;
@@ -277,7 +278,7 @@ GEXTEND Gram
     [ [ "using"; el = constr_with_bindings -> el ] ]
   ;
   with_names:
-    [ [ "as"; ipat = simple_intropattern -> Some ipat | -> None ] ]
+    [ [ "as"; ipat = simple_intropattern -> ipat | -> IntroAnonymous ] ]
   ;
   by_tactic:
     [ [ "by"; tac = tactic -> tac | -> TacId "" ] ]
@@ -325,9 +326,9 @@ GEXTEND Gram
 
       (* Begin compatibility *)
       | IDENT "assert"; id = lpar_id_coloneq; c = lconstr; ")" -> 
-	  TacAssert (None,Some (IntroIdentifier id),c)
+	  TacAssert (None,IntroIdentifier id,c)
       | IDENT "assert"; id = lpar_id_colon; c = lconstr; ")"; tac=by_tactic -> 
-	  TacAssert (Some tac,Some (IntroIdentifier id),c)
+	  TacAssert (Some tac,IntroIdentifier id,c)
       (* End compatibility *)
 
       | IDENT "assert"; c = constr; ipat = with_names; tac = by_tactic ->
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index c1eef07dcb..ea693afa43 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -348,23 +348,9 @@ 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
-  | [pl] ->
-      str "(" ++ hov 0 (prlist_with_sep pr_coma pr_intro_pattern pl) ++ str ")"
-  | pll ->
-      str "[" ++
-      hv 0 (prlist_with_sep pr_bar 
-        (fun l -> hov 0 (prlist_with_sep spc pr_intro_pattern l)) pll)
-      ++ str "]"
-
 let pr_with_names = function
-  | None -> mt ()
-  | Some ipat -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)
+  | IntroAnonymous -> mt ()
+  | ipat -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)
 
 let pr_pose prlc prc na c = match na with
   | Anonymous -> spc() ++ prc c
@@ -372,7 +358,7 @@ let pr_pose prlc prc na c = match na with
 
 let pr_assertion _prlc prc ipat c = match ipat with
 (* Use this "optimisation" or use only the general case ?
-  | Some (IntroIdentifier id) ->
+  | IntroIdentifier id ->
       spc() ++ surround (pr_intro_pattern ipat ++ str " :" ++ spc() ++ prlc c)
 *)
   | ipat ->
@@ -380,7 +366,7 @@ let pr_assertion _prlc prc ipat c = match ipat with
 
 let pr_assumption prlc prc ipat c = match ipat with
 (* Use this "optimisation" or use only the general case ?
-  | Some (IntroIdentifier id) ->
+  | IntroIdentifier id ->
       spc() ++ surround (pr_intro_pattern ipat ++ str " :" ++ spc() ++ prlc c)
 *)
   | ipat ->
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index 05faff2cd0..fd448281f6 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -77,8 +77,6 @@ val pr_extend :
   (tolerability -> glob_tactic_expr -> std_ppcmds) -> int ->
     string -> closed_generic_argument list -> std_ppcmds
 
-val pr_intro_pattern : intro_pattern_expr -> std_ppcmds
-
 val pr_raw_tactic : env -> raw_tactic_expr -> std_ppcmds
 
 val pr_raw_tactic_level : env -> tolerability -> raw_tactic_expr -> std_ppcmds
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 659f64c7b6..fcd21098df 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -58,6 +58,7 @@ let mlexpr_of_reference = function
 let mlexpr_of_intro_pattern = function
   | Genarg.IntroOrAndPattern _ -> failwith "mlexpr_of_intro_pattern: TODO"
   | Genarg.IntroWildcard -> <:expr< Genarg.IntroWildcard >>
+  | Genarg.IntroAnonymous -> <:expr< Genarg.IntroAnonymous >>
   | Genarg.IntroIdentifier id ->
       <:expr< Genarg.IntroIdentifier (mlexpr_of_ident $dloc$ id) >>
 
@@ -298,7 +299,7 @@ let rec mlexpr_of_atomic_tactic = function
   | Tacexpr.TacCut c ->
       <:expr< Tacexpr.TacCut $mlexpr_of_constr c$ >>
   | Tacexpr.TacAssert (t,ipat,c) ->
-      let ipat = mlexpr_of_option mlexpr_of_intro_pattern ipat in
+      let ipat = mlexpr_of_intro_pattern ipat in
       <:expr< Tacexpr.TacAssert $mlexpr_of_option mlexpr_of_tactic t$ $ipat$ 
 	      $mlexpr_of_constr c$ >>
   | Tacexpr.TacGeneralize cl ->
@@ -315,13 +316,13 @@ let rec mlexpr_of_atomic_tactic = function
       <:expr< Tacexpr.TacSimpleInduction ($mlexpr_of_quantified_hypothesis h$) >>
   | Tacexpr.TacNewInduction (c,cbo,ids) ->
       let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
-      let ids = mlexpr_of_option mlexpr_of_intro_pattern ids in
+      let ids = mlexpr_of_intro_pattern ids in
       <:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ $cbo$ $ids$>>
   | Tacexpr.TacSimpleDestruct h ->
       <:expr< Tacexpr.TacSimpleDestruct $mlexpr_of_quantified_hypothesis h$ >>
   | Tacexpr.TacNewDestruct (c,cbo,ids) ->
       let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
-      let ids = mlexpr_of_option mlexpr_of_intro_pattern ids in
+      let ids = mlexpr_of_intro_pattern ids in
       <:expr< Tacexpr.TacNewDestruct $mlexpr_of_induction_arg c$ $cbo$ $ids$ >>
 
   (* Context management *)