diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-28 09:24:15 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-28 09:24:15 +0000 |
commit | f7665a72dba3a896997220d738597cfe05b27990 (patch) | |
tree | 9bf47da71e2a912832199c6d13633d8ddee34678 /theories/Program/Equality.v | |
parent | 059a0622a512e40ffc1944cdc6084c3462aa85f9 (diff) |
Fixes in generalize_eqs/dependent induction to allow the user to specify
generalized variables himself.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11280 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Program/Equality.v')
-rw-r--r-- | theories/Program/Equality.v | 25 |
1 files changed, 19 insertions, 6 deletions
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 89e44c9bc..cd30d77ca 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -235,30 +235,43 @@ Ltac simpl_depind := subst* ; autoinjections ; try discriminates ; and starts a dependent induction using this tactic. *) Ltac do_depind tac H := + generalize_eqs_vars H ; tac H ; repeat progress simpl_depind. + +(** A variant where generalized variables should be given by the user. *) + +Ltac do_depind' tac H := generalize_eqs H ; tac H ; repeat progress simpl_depind. (** Calls [destruct] on the generalized hypothesis, results should be similar to inversion. *) Tactic Notation "dependent" "destruction" ident(H) := - do_depind ltac:(fun H => destruct H ; intros) H ; subst*. + do_depind ltac:(fun hyp => destruct hyp ; intros) H ; subst*. Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) := - do_depind ltac:(fun H => destruct H using c ; intros) H. + do_depind ltac:(fun hyp => destruct hyp using c ; intros) H. + +(** This tactic also generalizes the goal by the given variables before the induction. *) + +Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) := + do_depind' ltac:(fun hyp => revert l ; destruct hyp ; intros) H. + +Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := + do_depind' ltac:(fun hyp => revert l ; destruct hyp using c ; intros) H. (** Then we have wrappers for usual calls to induction. One can customize the induction tactic by writting another wrapper calling do_depind. *) Tactic Notation "dependent" "induction" ident(H) := - do_depind ltac:(fun H => induction H ; intros) H. + do_depind ltac:(fun hyp => induction hyp ; intros) H. Tactic Notation "dependent" "induction" ident(H) "using" constr(c) := - do_depind ltac:(fun H => induction H using c ; intros) H. + do_depind ltac:(fun hyp => induction hyp using c ; intros) H. (** This tactic also generalizes the goal by the given variables before the induction. *) Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := - do_depind ltac:(fun H => generalize l ; clear l ; induction H ; intros) H. + do_depind' ltac:(fun hyp => generalize l ; clear l ; induction hyp ; intros) H. Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := - do_depind ltac:(fun H => generalize l ; clear l ; induction H using c ; intros) H. + do_depind' ltac:(fun hyp => generalize l ; clear l ; induction hyp using c ; intros) H. |