From 14e4261beb81ba792dc1e42ddf52f24c04596150 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 4 Feb 2009 17:37:07 +0000
Subject: Report r11631 from 8.2 and handle non-dependent goals better in
 [dependent induction].

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11881 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Program/Equality.v | 17 +++++++++++------
 1 file changed, 11 insertions(+), 6 deletions(-)

(limited to 'theories/Program')

diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 1e19f66b81..be2f176d37 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -479,7 +479,12 @@ Ltac intro_prototypes :=
     | _ => idtac
   end.
 
-Ltac do_case p := destruct p || elim_case p || (case p ; clear p).
+Ltac introduce p := 
+  first [ match p with _ => idtac end (* Already there *)
+    | intros until p | intros ].
+
+Ltac do_case p := introduce p ; (destruct p || elim_case p || (case p ; clear p)).
+Ltac do_ind p := introduce p ; (induction p || elim_ind p).
 
 Ltac dep_elimify := match goal with [ |- ?T ] => change (block_dep_elim T) end.
 
@@ -530,7 +535,7 @@ Ltac do_depind' tac H :=
    By default, we don't try to generalize the hyp by its variable indices.  *)
 
 Tactic Notation "dependent" "destruction" ident(H) := 
-  do_depind' ltac:(fun hyp => destruct hyp) H.
+  do_depind' ltac:(fun hyp => do_case hyp) H.
 
 Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) := 
   do_depind' ltac:(fun hyp => destruct hyp using c) H.
@@ -538,7 +543,7 @@ Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) :=
 (** 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) H.
+  do_depind' ltac:(fun hyp => revert l ; do_case hyp) 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) H.
@@ -548,7 +553,7 @@ Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l)
    calling [induction]. *)
 
 Tactic Notation "dependent" "induction" ident(H) := 
-  do_depind ltac:(fun hyp => induction hyp) H.
+  do_depind ltac:(fun hyp => do_ind hyp) H.
 
 Tactic Notation "dependent" "induction" ident(H) "using" constr(c) := 
   do_depind ltac:(fun hyp => induction hyp using c) H.
@@ -556,7 +561,7 @@ Tactic Notation "dependent" "induction" ident(H) "using" constr(c) :=
 (** 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 hyp => generalize l ; clear l ; induction hyp) H.
+  do_depind' ltac:(fun hyp => generalize l ; clear l ; do_ind hyp) H.
 
 Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
   do_depind' ltac:(fun hyp => generalize l ; clear l ; induction hyp using c) H.
@@ -564,4 +569,4 @@ Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "
 Ltac simplify_IH_hyps := repeat
   match goal with
     | [ hyp : _ |- _ ] => specialize_hypothesis hyp
-  end.
+  end.
\ No newline at end of file
-- 
cgit v1.2.3