diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-19 17:56:29 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-19 17:56:29 +0000 |
| commit | d4f002fedb5669581ff2e270de798f05221c1313 (patch) | |
| tree | 54e0817c2a66bc525b9296c3be19634f1ab877bb /theories/Program | |
| parent | 7008fddba4b0a1ac9e46c0bf5af8ea09839232c8 (diff) | |
Suite 11472 et 11473
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11474 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Equality.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index d37fd62f6..4dd72b84d 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -364,10 +364,10 @@ Ltac simplify_one_dep_elim_term c := | eq (existT _ _ _) (existT _ _ _) -> _ => refine (simplification_existT _ _ _ _ _ _ _) | ?x = ?y -> _ => (* variables case *) (let hyp := fresh in intros hyp ; - move dependent hyp before x ; + move hyp before x ; generalize dependent x ; refine (solution_left _ _ _ _) ; intros until 0) || (let hyp := fresh in intros hyp ; - move dependent hyp before y ; + move 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 progress (intros H ; injection H ; clear H) @@ -557,4 +557,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.
\ No newline at end of file + end. |