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

14 files changed, 115 insertions, 125 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 9b5c14f239..8150d34e42 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -615,6 +615,7 @@ let rec xlate_intro_pattern =
 	   ll)
   | IntroWildcard -> CT_coerce_ID_to_INTRO_PATT(CT_ident "_" )
   | IntroIdentifier c -> CT_coerce_ID_to_INTRO_PATT(xlate_ident c)
+  | IntroAnonymous -> xlate_error "TODO: IntroAnonymous"
 
 let compute_INV_TYPE = function
    FullInversionClear -> CT_inv_clear
@@ -662,9 +663,9 @@ let xlate_one_unfold_block = function
   | (n::nums, qid) ->
       CT_unfold_occ(tac_qualid_to_ct_ID qid, nums_to_int_ne_list n nums);;
 
-let xlate_intro_patt_opt = function
-    None -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE
-  | Some fp -> CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT (xlate_intro_pattern fp)
+let xlate_with_names = function
+    IntroAnonymous -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE
+  | fp -> CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT (xlate_intro_pattern fp)
 
 let rawwit_main_tactic = rawwit_tactic Pcoq.Tactic.tactic_main_level
 
@@ -1127,12 +1128,12 @@ and xlate_tac =
     | (*For translating tactics/Inv.v *)
       TacInversion (NonDepInversion (k,idl,l),quant_hyp) ->
 	CT_inversion(compute_INV_TYPE k, xlate_quantified_hypothesis quant_hyp,
-		     xlate_intro_patt_opt l,
+		     xlate_with_names l,
 	             CT_id_list (List.map xlate_hyp idl))
     | TacInversion (DepInversion (k,copt,l),quant_hyp) ->
 	let id = xlate_quantified_hypothesis quant_hyp in
 	CT_depinversion (compute_INV_TYPE k, id, 
-			 xlate_intro_patt_opt l, xlate_formula_opt copt)
+			 xlate_with_names l, xlate_formula_opt copt)
     | TacInversion (InversionUsing (c,idlist), id) ->
 	let id = xlate_quantified_hypothesis id in
 	  CT_use_inversion (id, xlate_formula c,
@@ -1147,11 +1148,11 @@ and xlate_tac =
     | TacNewDestruct(a,b,c) ->
 	CT_new_destruct
 	  (xlate_int_or_constr a, xlate_using b, 
-	   xlate_intro_patt_opt c)
+	   xlate_with_names c)
     | TacNewInduction(a,b,c) ->
 	CT_new_induction
 	  (xlate_int_or_constr a, xlate_using b,
-	   xlate_intro_patt_opt c)
+	   xlate_with_names c)
     (*| TacInstantiate (a, b, cl) -> 
         CT_instantiate(CT_int a, xlate_formula b,
 		       assert false) *)
@@ -1162,13 +1163,13 @@ and xlate_tac =
 		  (* TODO LATER: This should be shared with Unfold,
 		     but the structures are different *)
 		  xlate_clause cl)
-    | TacAssert (None, Some (IntroIdentifier id), c) -> 
+    | TacAssert (None, IntroIdentifier id, c) -> 
         CT_assert(xlate_id_opt ((0,0),Name id), xlate_formula c)
-    | TacAssert (None, None, c) -> 
+    | TacAssert (None, IntroAnonymous, c) -> 
         CT_assert(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
-    | TacAssert (Some (TacId ""), Some (IntroIdentifier id), c) -> 
+    | TacAssert (Some (TacId ""), IntroIdentifier id, c) -> 
         CT_truecut(xlate_id_opt ((0,0),Name id), xlate_formula c)
-    | TacAssert (Some (TacId ""), None, c) -> 
+    | TacAssert (Some (TacId ""), IntroAnonymous, c) -> 
         CT_truecut(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
     | TacAssert _ ->
 	xlate_error "TODO: assert with 'as' and 'by' and pose proof with 'as'"
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 *)
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index c2b226281c..8f27088f0d 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -69,8 +69,8 @@ type inversion_kind =
   | FullInversionClear
 
 type ('c,'id) inversion_strength =
-  | NonDepInversion of inversion_kind * 'id list * intro_pattern_expr option
-  | DepInversion of inversion_kind * 'c option * intro_pattern_expr option
+  | NonDepInversion of inversion_kind * 'id list * intro_pattern_expr
+  | DepInversion of inversion_kind * 'c option * intro_pattern_expr
   | InversionUsing of 'c * 'id list
 
 type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
@@ -125,7 +125,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacCofix of identifier option
   | TacMutualCofix of identifier * (identifier * 'constr) list
   | TacCut of 'constr
-  | TacAssert of 'tac option * intro_pattern_expr option * 'constr
+  | TacAssert of 'tac option * intro_pattern_expr * 'constr
   | TacGeneralize of 'constr list
   | TacGeneralizeDep of 'constr
   | TacLetTac of name * 'constr * 'id gclause
@@ -134,10 +134,10 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   (* Derived basic tactics *)
   | TacSimpleInduction of quantified_hypothesis
   | TacNewInduction of 'constr induction_arg * 'constr with_bindings option
-      * intro_pattern_expr option
+      * intro_pattern_expr
   | TacSimpleDestruct of quantified_hypothesis
   | TacNewDestruct of 'constr induction_arg * 'constr with_bindings option
-      * intro_pattern_expr option
+      * intro_pattern_expr
 
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
   | TacDecomposeAnd of 'constr
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 3e66391cfc..6470b7a24d 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -58,10 +58,10 @@ val h_simple_induction   : quantified_hypothesis -> tactic
 val h_simple_destruct    : quantified_hypothesis -> tactic
 val h_new_induction   :
   constr induction_arg -> constr with_bindings option ->
-  intro_pattern_expr option -> tactic
+  intro_pattern_expr -> tactic
 val h_new_destruct    :
   constr induction_arg -> constr with_bindings option -> 
-  intro_pattern_expr option -> tactic
+  intro_pattern_expr -> tactic
 val h_specialize      : int option -> constr with_bindings -> tactic
 val h_lapply          : constr -> tactic
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 9597cfa41f..b799c939f8 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -377,6 +377,8 @@ let rewrite_equations_gene othin neqns ba gl =
 let rec get_names allow_conj = function
   | IntroWildcard ->
       error "Discarding pattern not allowed for inversion equations"
+  | IntroAnonymous ->
+      error "Anonymous pattern not allowed for inversion equations"
   | IntroOrAndPattern [l] -> 
       if allow_conj then
 	if l = [] then (None,[]) else
@@ -519,15 +521,15 @@ open Tacexpr
 
 let inv k = inv_gen false k NoDep
 
-let half_inv_tac id  = inv SimpleInversion None (NamedHyp id)
-let inv_tac id       = inv FullInversion None (NamedHyp id)
-let inv_clear_tac id = inv FullInversionClear None (NamedHyp id)
+let half_inv_tac id  = inv SimpleInversion IntroAnonymous (NamedHyp id)
+let inv_tac id       = inv FullInversion IntroAnonymous (NamedHyp id)
+let inv_clear_tac id = inv FullInversionClear IntroAnonymous (NamedHyp id)
 
 let dinv k c = inv_gen false k (Dep c)
 
-let half_dinv_tac id  = dinv SimpleInversion None None (NamedHyp id)
-let dinv_tac id       = dinv FullInversion None None (NamedHyp id)
-let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id)
+let half_dinv_tac id  = dinv SimpleInversion None IntroAnonymous (NamedHyp id)
+let dinv_tac id       = dinv FullInversion None IntroAnonymous (NamedHyp id)
+let dinv_clear_tac id = dinv FullInversionClear None IntroAnonymous (NamedHyp id)
 
 (* InvIn will bring the specified clauses into the conclusion, and then
  * perform inversion on the named hypothesis.  After, it will intro them
diff --git a/tactics/inv.mli b/tactics/inv.mli
index 7f80a03357..086c9d7cea 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -21,19 +21,19 @@ type inversion_status = Dep of constr option | NoDep
 
 val inv_gen :
   bool -> inversion_kind -> inversion_status ->
-    intro_pattern_expr option -> quantified_hypothesis -> tactic
+    intro_pattern_expr -> quantified_hypothesis -> tactic
 val invIn_gen :
-  inversion_kind -> intro_pattern_expr option -> identifier list -> 
+  inversion_kind -> intro_pattern_expr -> identifier list -> 
     quantified_hypothesis -> tactic
 
 val inv_clause :
-  inversion_kind -> intro_pattern_expr option -> identifier list ->
+  inversion_kind -> intro_pattern_expr -> identifier list ->
     quantified_hypothesis -> tactic
 
-val inv : inversion_kind -> intro_pattern_expr option ->
+val inv : inversion_kind -> intro_pattern_expr ->
   quantified_hypothesis -> tactic
 
-val dinv : inversion_kind -> constr option -> intro_pattern_expr option ->
+val dinv : inversion_kind -> constr option -> intro_pattern_expr ->
   quantified_hypothesis -> tactic
 
 val half_inv_tac : identifier -> tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index c3c01f3a2f..d1bf4389d9 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -417,10 +417,9 @@ let intern_reference strict ist r =
 let rec intern_intro_pattern lf ist = function
   | IntroOrAndPattern l ->
       IntroOrAndPattern (intern_case_intro_pattern lf ist l)
-  | IntroWildcard ->
-      IntroWildcard
   | IntroIdentifier id ->
       IntroIdentifier (intern_ident lf ist id)
+  | IntroWildcard | IntroAnonymous as x -> x
 
 and intern_case_intro_pattern lf ist =
   List.map (List.map (intern_intro_pattern lf ist))
@@ -513,10 +512,10 @@ let intern_redexp ist = function
 let intern_inversion_strength lf ist = function
   | NonDepInversion (k,idl,ids) ->
       NonDepInversion (k,List.map (intern_hyp_or_metaid ist) idl,
-      option_app (intern_intro_pattern lf ist) ids)
+      intern_intro_pattern lf ist ids)
   | DepInversion (k,copt,ids) ->
       DepInversion (k, option_app (intern_constr ist) copt,
-      option_app (intern_intro_pattern lf ist) ids)
+      intern_intro_pattern lf ist ids)
   | InversionUsing (c,idl) ->
       InversionUsing (intern_constr ist c, List.map (intern_hyp_or_metaid ist) idl)
 
@@ -633,7 +632,7 @@ let rec intern_atomic lf ist x =
   | TacCut c -> TacCut (intern_type ist c)
   | TacAssert (otac,ipat,c) ->
       TacAssert (option_app (intern_tactic ist) otac,
-                 option_app (intern_intro_pattern lf ist) ipat,
+                 intern_intro_pattern lf ist ipat,
                  intern_constr_gen (otac<>None) ist c)
   | TacGeneralize cl -> TacGeneralize (List.map (intern_constr ist) cl)
   | TacGeneralizeDep c -> TacGeneralizeDep (intern_constr ist c)
@@ -664,13 +663,13 @@ let rec intern_atomic lf ist x =
   | TacNewInduction (c,cbo,ids) ->
       TacNewInduction (intern_induction_arg ist c,
                option_app (intern_constr_with_bindings ist) cbo,
-               (option_app (intern_intro_pattern lf ist) ids))
+               (intern_intro_pattern lf ist ids))
   | TacSimpleDestruct h ->
       TacSimpleDestruct (intern_quantified_hypothesis ist h)
   | TacNewDestruct (c,cbo,ids) ->
       TacNewDestruct (intern_induction_arg ist c,
                option_app (intern_constr_with_bindings ist) cbo,
-	       (option_app (intern_intro_pattern lf ist) ids))
+	       (intern_intro_pattern lf ist ids))
   | TacDoubleInduction (h1,h2) ->
       let h1 = intern_quantified_hypothesis ist h1 in
       let h2 = intern_quantified_hypothesis ist h2 in
@@ -1138,7 +1137,7 @@ let rec intropattern_ids = function
   | IntroIdentifier id -> [id]
   | IntroOrAndPattern ll -> 
       List.flatten (List.map intropattern_ids (List.flatten ll))
-  | IntroWildcard -> []
+  | IntroWildcard | IntroAnonymous -> []
 
 let rec extract_ids = function
   | (id,VIntroPattern ipat)::tl -> intropattern_ids ipat @ extract_ids tl
@@ -1290,8 +1289,8 @@ let interp_constr_may_eval ist gl c =
 
 let rec interp_intro_pattern ist = function
   | IntroOrAndPattern l -> IntroOrAndPattern (interp_case_intro_pattern ist l)
-  | IntroWildcard -> IntroWildcard
   | IntroIdentifier id -> interp_intro_pattern_var ist id
+  | IntroWildcard | IntroAnonymous as x -> x
 
 and interp_case_intro_pattern ist =
   List.map (List.map (interp_intro_pattern ist))
@@ -1707,7 +1706,7 @@ and interp_atomic ist gl = function
       let c = (if t=None then pf_interp_constr else pf_interp_type) ist gl c in
       abstract_tactic (TacAssert (t,ipat,c))
         (Tactics.forward (option_app (interp_tactic ist) t)
-	  (option_app (interp_intro_pattern ist) ipat) c)
+	  (interp_intro_pattern ist ipat) c)
   | TacGeneralize cl -> h_generalize (List.map (pf_interp_constr ist gl) cl)
   | TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c)
   | TacLetTac (na,c,clp) ->
@@ -1737,13 +1736,13 @@ and interp_atomic ist gl = function
   | TacNewInduction (c,cbo,ids) ->
       h_new_induction (interp_induction_arg ist gl c)
         (option_app (interp_constr_with_bindings ist gl) cbo)
-        (option_app (interp_intro_pattern ist) ids)
+        (interp_intro_pattern ist ids)
   | TacSimpleDestruct h ->
       h_simple_destruct (interp_quantified_hypothesis ist h)
   | TacNewDestruct (c,cbo,ids) -> 
       h_new_destruct (interp_induction_arg ist gl c)
         (option_app (interp_constr_with_bindings ist gl) cbo)
-        (option_app (interp_intro_pattern ist) ids)
+        (interp_intro_pattern ist ids)
   | TacDoubleInduction (h1,h2) ->
       let h1 = interp_quantified_hypothesis ist h1 in
       let h2 = interp_quantified_hypothesis ist h2 in
@@ -1790,11 +1789,11 @@ and interp_atomic ist gl = function
   (* Equality and inversion *)
   | TacInversion (DepInversion (k,c,ids),hyp) ->
       Inv.dinv k (option_app (pf_interp_constr ist gl) c)
-        (option_app (interp_intro_pattern ist) ids)
+        (interp_intro_pattern ist ids)
         (interp_declared_or_quantified_hypothesis ist gl hyp)
   | TacInversion (NonDepInversion (k,idl,ids),hyp) ->
       Inv.inv_clause k 
-        (option_app (interp_intro_pattern ist) ids)
+        (interp_intro_pattern ist ids)
         (List.map (interp_hyp ist gl) idl)
         (interp_declared_or_quantified_hypothesis ist gl hyp)
   | TacInversion (InversionUsing (c,idl),hyp) ->
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 05eb17fe7b..517d774d4d 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -266,9 +266,9 @@ type branch_assumptions = {
   assums    : named_context}   (* the list of assumptions introduced *)
 
 let compute_induction_names n = function
-  | None ->
+  | IntroAnonymous ->
       Array.make n []
-  | Some (IntroOrAndPattern names) when List.length names = n ->
+  | IntroOrAndPattern names when List.length names = n ->
       Array.of_list names
   | _ ->
       errorlabstrm "" (str "Expects " ++ int n ++ str " lists of names")
@@ -377,7 +377,7 @@ let elimination_then_using tac predicate (indbindings,elimbindings) c gl =
   let elim =
     Indrec.lookup_eliminator ind (elimination_sort_of_goal gl) in
   general_elim_then_using
-    elim true None tac predicate (indbindings,elimbindings) c gl
+    elim true IntroAnonymous tac predicate (indbindings,elimbindings) c gl
 
 
 let elimination_then tac        = elimination_then_using tac None 
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 67dbcfc0f4..699c0d7801 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -129,13 +129,13 @@ type branch_assumptions = {
 
 (* Useful for [as intro_pattern] modifier *)
 val compute_induction_names : 
-  int -> intro_pattern_expr option -> intro_pattern_expr list array
+  int -> intro_pattern_expr -> intro_pattern_expr list array
 
 val elimination_sort_of_goal : goal sigma -> sorts_family
 val elimination_sort_of_hyp  : identifier -> goal sigma -> sorts_family
 
 val general_elim_then_using :
-  constr -> (* isrec: *) bool -> intro_pattern_expr option ->
+  constr -> (* isrec: *) bool -> intro_pattern_expr ->
     (branch_args -> tactic) -> constr option -> 
       (arg_bindings * arg_bindings) -> constr -> tactic
 	  
@@ -148,11 +148,11 @@ val elimination_then :
     (arg_bindings * arg_bindings) -> constr -> tactic
 
 val case_then_using :
-  intro_pattern_expr option -> (branch_args -> tactic) -> 
+  intro_pattern_expr -> (branch_args -> tactic) -> 
     constr option -> (arg_bindings * arg_bindings) -> constr -> tactic
 
 val case_nodep_then_using :
-  intro_pattern_expr option -> (branch_args -> tactic) -> 
+  intro_pattern_expr -> (branch_args -> tactic) -> 
     constr option -> (arg_bindings * arg_bindings) -> constr -> tactic
 
 val simple_elimination_then :
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b277df0e00..36b948862a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -798,7 +798,7 @@ let clear_last = tclLAST_HYP (fun c -> (clear [destVar c]))
 let case_last  = tclLAST_HYP simplest_case
 
 let rec explicit_intro_names = function
-| IntroWildcard :: l -> explicit_intro_names l
+| (IntroWildcard | IntroAnonymous) :: l -> explicit_intro_names l
 | IntroIdentifier id :: l -> id :: explicit_intro_names l
 | IntroOrAndPattern ll :: l' -> 
     List.flatten (List.map (fun l -> explicit_intro_names (l@l')) ll)
@@ -808,26 +808,33 @@ let rec explicit_intro_names = function
      to ensure that dependent hypotheses are cleared in the right
      dependency order (see bug #1000); we use fresh names, not used in
      the tactic, for the hyps to clear *)
-let rec intros_patterns thin destopt = function
+let rec intros_patterns avoid thin destopt = function
   | IntroWildcard :: l ->
       tclTHEN 
-        (intro_gen (IntroAvoid (explicit_intro_names l)) None true)
-        (onLastHyp (fun id -> intros_patterns (id::thin) destopt l))
+        (intro_gen (IntroAvoid (avoid@explicit_intro_names l)) None true)
+        (onLastHyp (fun id ->
+	  tclORELSE
+	    (tclTHEN (clear [id]) (intros_patterns avoid thin destopt l))
+	    (intros_patterns avoid (id::thin) destopt l)))
   | IntroIdentifier id :: l ->
       tclTHEN
         (intro_gen (IntroMustBe id) destopt true)
-        (intros_patterns thin destopt l)
+        (intros_patterns avoid thin destopt l)
+  | IntroAnonymous :: l ->
+      tclTHEN
+        (intro_gen (IntroAvoid (avoid@explicit_intro_names l)) destopt true)
+        (intros_patterns avoid thin destopt l)
   | IntroOrAndPattern ll :: l' ->
       tclTHEN
         introf
         (tclTHENS
 	  (tclTHEN case_last clear_last)
-	  (List.map (fun l -> intros_patterns thin destopt (l@l')) ll))
+	  (List.map (fun l -> intros_patterns avoid thin destopt (l@l')) ll))
   | [] -> clear thin
 
-let intros_pattern = intros_patterns []
+let intros_pattern = intros_patterns [] []
 
-let intro_pattern destopt pat = intros_patterns [] destopt [pat]
+let intro_pattern destopt pat = intros_patterns [] [] destopt [pat]
 
 let intro_patterns = function 
   | [] -> tclREPEAT intro
@@ -843,17 +850,17 @@ let xid = id_of_string "X"
 let make_id s = fresh_id [] (match s with Prop _ -> hid | Type _ -> xid)
 
 let prepare_intros s ipat gl = match ipat with
-  | None -> make_id s gl, tclIDTAC
-  | Some IntroWildcard -> let id = make_id s gl in id, thin [id]
-  | Some (IntroIdentifier id) -> id, tclIDTAC
-  | Some (IntroOrAndPattern ll) -> make_id s gl, 
-        (tclTHENS 
-	  (tclTHEN case_last clear_last)
-	  (List.map (intros_patterns [] None) ll))
+  | IntroAnonymous -> make_id s gl, tclIDTAC
+  | IntroWildcard -> let id = make_id s gl in id, thin [id]
+  | IntroIdentifier id -> id, tclIDTAC
+  | IntroOrAndPattern ll -> make_id s gl, 
+    (tclTHENS 
+      (tclTHEN case_last clear_last)
+      (List.map (intros_pattern None) ll))
 
 let ipat_of_name = function
-  | Anonymous -> None
-  | Name id -> Some (IntroIdentifier id)
+  | Anonymous -> IntroAnonymous
+  | Name id -> IntroIdentifier id
 
 let assert_as first ipat c gl =
   match kind_of_term (hnf_type_of gl c) with
@@ -1124,6 +1131,14 @@ let rec first_name_buggy = function
   | IntroOrAndPattern ((p::_)::_) -> first_name_buggy p
   | IntroWildcard -> None
   | IntroIdentifier id -> Some id
+  | IntroAnonymous -> assert false
+
+let consume_pattern avoid id gl = function
+  | [] -> (IntroIdentifier (fresh_id avoid id gl), [])
+  | IntroAnonymous::names ->
+      let avoid = avoid@explicit_intro_names names in
+      (IntroIdentifier (fresh_id avoid id gl), names)
+  | pat::names -> (pat,names)
 
 type elim_arg_kind = RecArg | IndArg | OtherArg
 
@@ -1134,43 +1149,30 @@ let induct_discharge statuslists destopt avoid' (avoid,ra) names gl =
   let rec peel_tac ra names gl = match ra with
     | (RecArg,recvarname) ::
         (IndArg,hyprecname) :: ra' ->
-        let recpat,hyprec,names = match names with
-          | [] ->
-              let idrec = fresh_id avoid recvarname gl in
-              let idhyp = fresh_id avoid hyprecname gl in
-              (IntroIdentifier idrec, IntroIdentifier idhyp, [])
+        let recpat,names = match names with
           | [IntroIdentifier id as pat] ->
               let id = next_ident_away (add_prefix "IH" id) avoid in
-	      (pat, IntroIdentifier id, [])
-	  | [pat] ->
-              let idhyp = (fresh_id avoid hyprecname gl) in
-	      (pat, IntroIdentifier idhyp, [])
-          | pat1::pat2::names -> (pat1,pat2,names) in
+	      (pat, [IntroIdentifier id])
+          | _ -> consume_pattern avoid recvarname gl names in
+        let hyprec,names = consume_pattern avoid hyprecname gl names in
 	(* This is buggy for intro-or-patterns with different first hypnames *)
 	if !tophyp=None then tophyp := first_name_buggy hyprec;
         tclTHENLIST
-	  [ intros_pattern destopt [recpat];
-	    intros_pattern None [hyprec];
+	  [ intros_patterns avoid [] destopt [recpat];
+	    intros_patterns avoid [] None [hyprec];
 	    peel_tac ra' names ] gl
     | (IndArg,hyprecname) :: ra' ->
 	(* Rem: does not happen in Coq schemes, only in user-defined schemes *)
-        let pat,names = match names with
-          | [] -> IntroIdentifier (fresh_id avoid hyprecname gl), []
-	  | pat::names -> pat,names in
-	tclTHEN (intros_pattern destopt [pat]) (peel_tac ra' names) gl
+        let pat,names = consume_pattern avoid hyprecname gl names in
+	tclTHEN (intros_patterns avoid [] destopt [pat]) (peel_tac ra' names) gl
     | (RecArg,recvarname) :: ra' ->
-        let introtac,names = match names with
-          | [] -> 
-              let id = fresh_id avoid recvarname gl in
-	      intro_gen (IntroMustBe id) destopt false, []
-          | pat::names ->
-	      intros_pattern destopt [pat],names in
-	tclTHEN introtac (peel_tac ra' names) gl
+        let pat,names = consume_pattern avoid recvarname gl names in
+	tclTHEN (intros_patterns avoid [] destopt [pat]) (peel_tac ra' names) gl
     | (OtherArg,_) :: ra' ->
-        let introtac,names = match names with
-          | [] -> intro_gen (IntroAvoid avoid) destopt false, []
-          | pat::names -> intros_pattern destopt [pat],names in
-	tclTHEN introtac (peel_tac ra' names) gl
+        let pat,names = match names with
+          | [] -> IntroAnonymous, []
+          | pat::names -> pat,names in
+	tclTHEN (intros_patterns avoid [] destopt [pat]) (peel_tac ra' names) gl
     | [] ->
         check_unused_names names;
         tclIDTAC gl
@@ -1491,7 +1493,6 @@ let induction_from_context isrec elim_info hyp0 names gl =
   let (statlists,lhyp0,indhyps,deps) = cook_sign hyp0 indvars env in
   let tmpcl = it_mkNamedProd_or_LetIn (pf_concl gl) deps in
   let names = compute_induction_names (Array.length indsign) names in
-  (* End translator *)
   let dephyps = List.map (fun (id,_,_) -> id) deps in
   let args =
     List.fold_left
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 95a2facc07..cf0b06862e 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -178,7 +178,7 @@ val elim          : constr with_bindings -> constr with_bindings option -> tacti
 val simple_induct : quantified_hypothesis -> tactic
 
 val new_induct : constr induction_arg -> constr with_bindings option ->
-  intro_pattern_expr option -> tactic
+  intro_pattern_expr -> tactic
 
 (*s Case analysis tactics. *)
 
@@ -187,7 +187,7 @@ val simplest_case         : constr -> tactic
 
 val simple_destruct          : quantified_hypothesis -> tactic
 val new_destruct : constr induction_arg -> constr with_bindings option ->
-  intro_pattern_expr option -> tactic
+  intro_pattern_expr -> tactic
 
 (*s Eliminations giving the type instead of the proof. *)
 
@@ -239,11 +239,12 @@ val cut_replacing               :
   identifier -> constr -> (tactic -> tactic) -> tactic
 val cut_in_parallel             : constr list -> tactic
 
-val assert_as : bool -> intro_pattern_expr option -> constr -> tactic
+val assert_as : bool -> intro_pattern_expr -> constr -> tactic
+val forward   : tactic option -> intro_pattern_expr -> constr -> tactic
+
 val true_cut                    : name -> constr -> tactic
 val letin_tac                   : bool -> name -> constr -> clause -> tactic
 val assert_tac                  : bool -> name -> constr -> tactic
-val forward    : tactic option -> intro_pattern_expr option -> constr -> tactic
 val generalize                  : constr list -> tactic
 val generalize_dep              : constr  -> tactic