From 9dacc590c604290d9556d9368c5c735321e01e90 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 26 Feb 2015 09:58:46 +0100 Subject: Revert "Fixing bug #4035 (support for dependent destruction within ltac code)." This reverts commit 4e6c9891140932f452bb5ac8960d597b0b5fde1d, which was breaking compatibility because one could no longer use names of foralls in the goal without introducting them. Probably not good style, but it did break many existing developments including CompCert. Closes #4093 but reopens #4035. --- theories/Program/Equality.v | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'theories/Program') diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 4b0287317..ae6fe7dd0 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -433,40 +433,40 @@ Ltac do_depelim' rev tac H := (** Calls [destruct] on the generalized hypothesis, results should be similar to inversion. By default, we don't try to generalize the hyp by its variable indices. *) -Tactic Notation "dependent" "destruction" hyp(H) := +Tactic Notation "dependent" "destruction" ident(H) := do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => do_case hyp) H. -Tactic Notation "dependent" "destruction" hyp(H) "using" constr(c) := +Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) := do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => destruct hyp using c) H. (** This tactic also generalizes the goal by the given variables before the elimination. *) -Tactic Notation "dependent" "destruction" hyp(H) "generalizing" ne_hyp_list(l) := +Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) := do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => do_case hyp) H. -Tactic Notation "dependent" "destruction" hyp(H) "generalizing" ne_hyp_list(l) "using" constr(c) := +Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => destruct hyp using c) H. (** Then we have wrappers for usual calls to induction. One can customize the induction tactic by writting another wrapper calling do_depelim. We suppose the hyp has to be generalized before calling [induction]. *) -Tactic Notation "dependent" "induction" hyp(H) := +Tactic Notation "dependent" "induction" ident(H) := do_depind ltac:(fun hyp => do_ind hyp) H. -Tactic Notation "dependent" "induction" hyp(H) "using" constr(c) := +Tactic Notation "dependent" "induction" ident(H) "using" constr(c) := do_depind ltac:(fun hyp => induction hyp using c) H. (** This tactic also generalizes the goal by the given variables before the induction. *) -Tactic Notation "dependent" "induction" hyp(H) "generalizing" ne_hyp_list(l) := +Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => do_ind hyp) H. -Tactic Notation "dependent" "induction" hyp(H) "generalizing" ne_hyp_list(l) "using" constr(c) := +Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => induction hyp using c) H. -Tactic Notation "dependent" "induction" hyp(H) "in" ne_hyp_list(l) := +Tactic Notation "dependent" "induction" ident(H) "in" ne_hyp_list(l) := do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => induction hyp in l) H. -Tactic Notation "dependent" "induction" hyp(H) "in" ne_hyp_list(l) "using" constr(c) := +Tactic Notation "dependent" "induction" ident(H) "in" ne_hyp_list(l) "using" constr(c) := do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => induction hyp in l using c) H. -- cgit v1.2.3