diff options
| -rw-r--r-- | tactics/tactics.ml | 2 | ||||
| -rw-r--r-- | test-suite/success/intros.v | 10 |
2 files changed, 11 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index bbee0a2a79..0235126cc0 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2122,7 +2122,7 @@ let make_tmp_naming avoid l = function 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) + | pat -> NamingAvoid(avoid@explicit_intro_names ((dloc,IntroAction pat)::l)) let fit_bound n = function | None -> true diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index 4959b65788..ae1694c58c 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -51,3 +51,13 @@ Fail clear H0. match goal with H:_ |- _ => clear H end. (* clear H1:False *) match goal with H:_ |- _ => exact H end. (* check that next hyp shows 0=0 *) Qed. + +Goal (True -> 0=0) -> True -> 0=0. +intros H H1/H. +exact H1. +Qed. + +Goal forall n, n = S n -> 0=0. +intros n H/n_Sn. +destruct H. +Qed. |