diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-02-26 09:58:46 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-02-26 09:58:46 +0100 |
| commit | 9dacc590c604290d9556d9368c5c735321e01e90 (patch) | |
| tree | 887fd2572a386adca5148619ca8f7b09caac6374 /theories/Program | |
| parent | d82f2c96e73484aae7e6f9e014823065584fbc6e (diff) | |
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.
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Equality.v | 20 |
1 files changed, 10 insertions, 10 deletions
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. |