Seeing IntroWildcard as an action intro pattern rather than as a naming pattern

(the action is "clear").

Added subst_intropattern which was missing since the introduction of
ApplyOn intro patterns.

Still to do: make "intros _ ?id" working without interferences when
"id" is precisely the internal name used for hypotheses to discard.

12 files changed, 48 insertions, 28 deletions

diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 25d4c0b23c..1eadf7dfdc 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -62,7 +62,6 @@ let mlexpr_of_intro_pattern_disjunctive = function
   _ -> failwith "mlexpr_of_intro_pattern_disjunctive: TODO"
 
 let mlexpr_of_intro_pattern_naming = function
-  | Misctypes.IntroWildcard -> <:expr< Misctypes.IntroWildcard >>
   | Misctypes.IntroAnonymous -> <:expr< Misctypes.IntroAnonymous >>
   | Misctypes.IntroFresh id -> <:expr< Misctypes.IntroFresh (mlexpr_of_ident $dloc$ id) >>
   | Misctypes.IntroIdentifier id ->
diff --git a/intf/misctypes.mli b/intf/misctypes.mli
index c61da0e306..2c8ac3a693 100644
--- a/intf/misctypes.mli
+++ b/intf/misctypes.mli
@@ -21,11 +21,11 @@ type 'constr intro_pattern_expr =
   | IntroNaming of intro_pattern_naming_expr
   | IntroAction of 'constr intro_pattern_action_expr
 and intro_pattern_naming_expr =
-  | IntroWildcard
   | IntroIdentifier of Id.t
   | IntroFresh of Id.t
   | IntroAnonymous
 and 'constr intro_pattern_action_expr =
+  | IntroWildcard
   | IntroOrAndPattern of 'constr or_and_intro_pattern_expr
   | IntroInjection of (Loc.t * 'constr intro_pattern_expr) list
   | IntroApplyOn of 'constr * (Loc.t * 'constr intro_pattern_expr)
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 3e83e2ca18..80edccfeb1 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -296,8 +296,7 @@ GEXTEND Gram
   naming_intropattern:
     [ [ prefix = pattern_ident -> IntroFresh prefix
       | "?" -> IntroAnonymous
-      | id = ident -> IntroIdentifier id
-      | "_" -> IntroWildcard ] ]
+      | id = ident -> IntroIdentifier id ] ]
   ;
   nonsimple_intropattern:
     [ [ l = simple_intropattern -> l
@@ -307,6 +306,7 @@ GEXTEND Gram
   simple_intropattern:
     [ [ pat = or_and_intropattern -> !@loc, IntroAction (IntroOrAndPattern pat)
       | pat = equality_intropattern -> !@loc, IntroAction pat
+      | "_" -> !@loc, IntroAction IntroWildcard 
       | pat = simple_intropattern; "/"; c = constr ->
           !@loc, IntroAction (IntroApplyOn (c,pat))
       | pat = naming_intropattern -> !@loc, IntroNaming pat ] ]
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index ffc1ea2a77..826fd59ba8 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -612,8 +612,7 @@ let add_name_newly_undefined naming evk evi (evtoid,idtoev) =
           (Loc.ghost,"",str "Already an existential evar of name " ++ pr_id id);
       id'
   | Misctypes.IntroFresh id ->
-      Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev)
-  | Misctypes.IntroWildcard -> assert false in
+      Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in
   (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
 
 let add_name_undefined naming evk evi (evtoid,idtoev as evar_names) =
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index e96e3a8b7f..83e33f84ea 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -34,6 +34,5 @@ let glob_sort_eq g1 g2 = match g1, g2 with
 let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with
 | IntroAnonymous, IntroAnonymous -> true
 | IntroIdentifier id1, IntroIdentifier id2 -> Names.Id.equal id1 id2
-| IntroWildcard, IntroWildcard -> true
 | IntroFresh id1, IntroFresh id2 -> Names.Id.equal id1 id2
 | _ -> false
diff --git a/printing/miscprint.ml b/printing/miscprint.ml
index 682cc3abe7..b47deab0fa 100644
--- a/printing/miscprint.ml
+++ b/printing/miscprint.ml
@@ -18,12 +18,12 @@ let rec pr_intro_pattern prc (_,pat) = match pat with
   | IntroAction p -> pr_intro_pattern_action prc p
 
 and pr_intro_pattern_naming = function
-  | IntroWildcard -> str "_"
   | IntroIdentifier id -> Nameops.pr_id id
   | IntroFresh id -> str "?" ++ Nameops.pr_id id
   | IntroAnonymous -> str "?"
 
 and pr_intro_pattern_action prc = function
+  | IntroWildcard -> str "_"
   | IntroOrAndPattern pll -> pr_or_and_intro_pattern prc pll
   | IntroInjection pl ->
       str "[=" ++ hv 0 (prlist_with_sep spc (pr_intro_pattern prc) pl) ++
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 081b62b18c..457068c6cd 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -286,12 +286,12 @@ let error_too_many_names pats =
     str ".")
 
 let rec get_names (allow_conj,issimple) (loc,pat as x) = match pat with
-  | IntroNaming IntroWildcard ->
-      error "Discarding pattern not allowed for inversion equations."
   | IntroNaming IntroAnonymous | IntroForthcoming _ ->
       error "Anonymous pattern not allowed for inversion equations."
   | IntroNaming (IntroFresh _) ->
       error "Fresh pattern not allowed for inversion equations."
+  | IntroAction IntroWildcard ->
+      error "Discarding pattern not allowed for inversion equations."
   | IntroAction (IntroRewrite _) ->
       error "Rewriting pattern not allowed for inversion equations."
   | IntroAction (IntroOrAndPattern [[]]) when allow_conj -> (None, [])
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 23be275520..08dd0dff48 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -254,14 +254,14 @@ and intern_intro_pattern_naming lf ist = function
       IntroIdentifier (intern_ident lf ist id)
   | IntroFresh id ->
       IntroFresh (intern_ident lf ist id)
-  | IntroWildcard | IntroAnonymous as x -> x
+  | IntroAnonymous as x -> x
 
 and intern_intro_pattern_action lf ist = function
   | IntroOrAndPattern l ->
       IntroOrAndPattern (intern_or_and_intro_pattern lf ist l)
   | IntroInjection l ->
       IntroInjection (List.map (intern_intro_pattern lf ist) l)
-  | IntroRewrite _ as x -> x
+  | IntroWildcard | IntroRewrite _ as x -> x
   | IntroApplyOn (c,pat) ->
       IntroApplyOn (intern_constr ist c, intern_intro_pattern lf ist pat)
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 991eac57ed..cd460ebbe7 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -423,8 +423,8 @@ let rec intropattern_ids (loc,pat) = match pat with
   | IntroAction (IntroInjection l) ->
       List.flatten (List.map intropattern_ids l)
   | IntroAction (IntroApplyOn (c,pat)) -> intropattern_ids pat
-  | IntroNaming (IntroWildcard | IntroAnonymous | IntroFresh _)
-  | IntroAction (IntroRewrite _)
+  | IntroNaming (IntroAnonymous | IntroFresh _)
+  | IntroAction (IntroWildcard | IntroRewrite _)
   | IntroForthcoming _ -> []
 
 let extract_ids ids lfun =
@@ -799,7 +799,7 @@ let rec interp_intro_pattern ist env sigma = function
 and interp_intro_pattern_naming loc ist env sigma = function
   | IntroFresh id -> IntroFresh (interp_fresh_ident ist env sigma id)
   | IntroIdentifier id -> interp_intro_pattern_naming_var loc ist env sigma id
-  | (IntroWildcard | IntroAnonymous) as x -> x
+  | IntroAnonymous as x -> x
 
 and interp_intro_pattern_action ist env sigma = function
   | IntroOrAndPattern l ->
@@ -812,7 +812,7 @@ and interp_intro_pattern_action ist env sigma = function
       let c = fun env sigma -> interp_constr ist env sigma c in
       let sigma,ipat = interp_intro_pattern ist env sigma ipat in
       sigma, IntroApplyOn (c,ipat)
-  | IntroRewrite _ as x -> sigma, x
+  | IntroWildcard | IntroRewrite _ as x -> sigma, x
 
 and interp_or_and_intro_pattern ist env sigma =
   List.fold_map (interp_intro_pattern_list_as_list ist env) sigma
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index b1d03f86e2..27d0d7e0fd 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -47,6 +47,18 @@ let subst_glob_with_bindings subst (c,bl) =
 let subst_glob_with_bindings_arg subst (clear,c) =
   (clear,subst_glob_with_bindings subst c)
 
+let rec subst_intro_pattern subst = function
+  | loc,IntroAction p -> loc, IntroAction (subst_intro_pattern_action subst p)
+  | loc, IntroNaming _ | loc, IntroForthcoming _ as x -> x
+
+and subst_intro_pattern_action subst = function
+  | IntroApplyOn (t,pat) ->
+      IntroApplyOn (subst_glob_constr subst t,subst_intro_pattern subst pat)
+  | IntroOrAndPattern l ->
+      IntroOrAndPattern (List.map (List.map (subst_intro_pattern subst)) l)
+  | IntroInjection l -> IntroInjection (List.map (subst_intro_pattern subst) l)
+  | IntroWildcard | IntroRewrite _ as x -> x
+
 let subst_induction_arg subst = function
   | clear,ElimOnConstr c -> clear,ElimOnConstr (subst_glob_with_bindings subst c)
   | clear,ElimOnAnonHyp n as x -> x
@@ -135,7 +147,8 @@ let rec subst_match_goal_hyps subst = function
 
 let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   (* Basic tactics *)
-  | TacIntroPattern _ | TacIntroMove _ as x -> x
+  | TacIntroPattern l -> TacIntroPattern (List.map (subst_intro_pattern subst) l)
+  | TacIntroMove _ as x -> x
   | TacExact c -> TacExact (subst_glob_constr subst c)
   | TacApply (a,ev,cb,cl) ->
       TacApply (a,ev,List.map (subst_glob_with_bindings_arg subst) cb,cl)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 69a72db4f7..2ccad790f1 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1852,8 +1852,6 @@ let rec prepare_naming loc = function
   | IntroIdentifier id -> NamingMustBe (loc,id)
   | IntroAnonymous -> NamingAvoid []
   | IntroFresh id -> NamingBasedOn (id,[])
-  | IntroWildcard ->
-      error "Did you really mind erasing the newly generated hypothesis?"
 
 let rec explicit_intro_names = function
 | (_, IntroForthcoming _) :: l -> explicit_intro_names l
@@ -1864,8 +1862,8 @@ let rec explicit_intro_names = function
     explicit_intro_names (l@l')
 | (_, IntroAction (IntroApplyOn (c,pat))) :: l' ->
     explicit_intro_names (pat::l')
-| (_, (IntroNaming (IntroWildcard | IntroAnonymous | IntroFresh _)
-     | IntroAction (IntroRewrite _))) :: l ->
+| (_, (IntroNaming (IntroAnonymous | IntroFresh _)
+     | IntroAction (IntroWildcard | IntroRewrite _))) :: l ->
      explicit_intro_names l
 | [] -> []
 
@@ -1884,6 +1882,16 @@ let check_thin_clash_then id thin avoid tac =
   else
     tac thin
 
+let make_tmp_naming avoid l = function
+  (* In theory, we could use a tmp id like "wild_id" for all actions
+     but we prefer to avoid it to avoid this kind of "ugly" names *)
+  (* Alternatively, we could have called check_thin_clash_then on
+     IntroAnonymous, but at the cost of a "renaming"; Note that in the
+     case of IntroFresh, we should use check_thin_clash_then anyway to
+     prevent the case of an IntroFresh precisely using the wild_id *)
+  | IntroWildcard -> NamingBasedOn (wild_id,avoid@explicit_intro_names l)
+  | _ -> NamingAvoid(avoid@explicit_intro_names l)
+
 let fit_bound n = function
   | None -> true
   | Some (use_bound,n') -> not use_bound || n = n'
@@ -1912,7 +1920,7 @@ let rec intro_patterns_core b avoid ids thin destopt bound n tac = function
         (fun ids -> intro_patterns_core b avoid ids thin destopt bound
           (n+List.length ids) tac l)
   | IntroAction pat ->
-      intro_then_gen (NamingAvoid(avoid@explicit_intro_names l))
+      intro_then_gen (make_tmp_naming avoid l pat)
 	MoveLast true false
         (intro_pattern_action loc (b || not (List.is_empty l)) false pat thin
           (fun thin bound' -> intro_patterns_core b avoid ids thin destopt bound' 0
@@ -1923,10 +1931,6 @@ let rec intro_patterns_core b avoid ids thin destopt bound n tac = function
 
 and intro_pattern_naming loc b avoid ids pat thin destopt bound n tac l =
   match pat with
-  | IntroWildcard ->
-      intro_then_gen (NamingBasedOn(wild_id,avoid@explicit_intro_names l))
-	MoveLast true false
-        (fun id -> intro_patterns_core b avoid ids ((loc,id)::thin) destopt bound (n+1) tac l)
   | IntroIdentifier id ->
       check_thin_clash_then id thin avoid (fun thin ->
         intro_then_gen (NamingMustBe (loc,id)) destopt true false
@@ -1942,6 +1946,8 @@ and intro_pattern_naming loc b avoid ids pat thin destopt bound n tac l =
         (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound (n+1) tac l)
 
 and intro_pattern_action loc b style pat thin tac id = match pat with
+  | IntroWildcard ->
+      tac ((loc,id)::thin) None []
   | IntroOrAndPattern ll ->
       intro_or_and_pattern loc b ll thin tac id
   | IntroInjection l' ->
@@ -2091,8 +2097,7 @@ let letin_tac_gen with_eq abs ty =
           let heq = match ido with
             | IntroAnonymous -> new_fresh_id [id] (add_prefix "Heq" id) gl
 	    | IntroFresh heq_base -> new_fresh_id [id] heq_base gl
-            | IntroIdentifier id -> id
-	    | _ -> Errors.error "Expect an introduction pattern naming one hypothesis." in
+            | IntroIdentifier id -> id in
           let eqdata = build_coq_eq_data () in
           let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in
           let sigma, eq = Evd.fresh_global env (Proofview.Goal.sigma gl) eqdata.eq in
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index bb9fc0c50d..9443d01e3b 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -28,3 +28,8 @@ Goal forall n p, n + p = 0.
 intros [|*]; intro p.
 Abort.
 
+(* Check non-interference of "_" with name generation *)
+Goal True -> True -> True.
+intros _ ?.
+exact H.
+Qed.