Various little improvements:

- A new [dependent pattern] tactic to do a pattern on an object in an
inductive family and generalize by both the indexes and the object
itself. Useful to prepare a goal for elimination with a dependent
principle.
- Better dependent elimination simplification tactic that doesn't
throw away non-dependent equalities if they can't be injected.
- Add [fold_sub] and [unfold_sub] tactics for folding/unfolding
well-founded definitions using measures built by Program.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11420 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 4 deletions

diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 2b914ace7..d37fd62f6 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -359,9 +359,9 @@ Definition block_dep_elim {A : Type} (a : A) := a.
 
 Ltac simplify_one_dep_elim_term c :=
   match c with
-    | @JMeq ?A ?a ?A ?b -> _ => refine (simplification_heq _ _ _ _ _)
+    | @JMeq _ _ _ _ -> _ => refine (simplification_heq _ _ _ _ _)
     | ?t = ?t -> _ => intros _ || refine (simplification_K _ t _ _)
-    | eq (existT ?P ?p _) (existT ?P ?p _) -> _ => refine (simplification_existT _ _ _ _ _ _ _)
+    | eq (existT _ _ _) (existT _ _ _) -> _ => refine (simplification_existT _ _ _ _ _ _ _)
     | ?x = ?y -> _ => (* variables case *)
       (let hyp := fresh in intros hyp ;
         move dependent hyp before x ;
@@ -370,11 +370,12 @@ Ltac simplify_one_dep_elim_term c :=
         move dependent hyp before y ;
           generalize dependent y ; refine (solution_right _ _ _ _) ; intros until 0)
     | @eq ?A ?t ?u -> ?P => apply (noConfusion (I:=A) P)
-    | ?f ?x = ?g ?y -> _ => let H := fresh in intros H ; injection H ; clear H
+    | ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; injection H ; clear H)
     | ?t = ?u -> _ => let hyp := fresh in
       intros hyp ; elimtype False ; discriminate
     | ?x = ?y -> _ => let hyp := fresh in
-      intros hyp ; case hyp ; clear hyp
+      intros hyp ; (try (clear hyp ; (* If non dependent, don't clear it! *) fail 1)) ;
+        case hyp ; clear hyp
     | block_dep_elim ?T => fail 1 (* Do not put any part of the rhs in the hyps *)
     | _ => intro
   end.