diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-01-02 13:26:08 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-01-02 13:26:08 +0000 |
commit | 640a6d2f48ba07b51bcabc4235eaa4a497f4c263 (patch) | |
tree | dc32022e578a0d8b15a5e442ba123428e4949768 /test-suite/success/dependentind.v | |
parent | c47a4f906b9427c93db441de30dd69898d42d449 (diff) |
Better resolution of implicit parameters in typeclass binders, add extensionality tactic to apply the axiom properly and fix test-suite.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10415 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/dependentind.v')
-rw-r--r-- | test-suite/success/dependentind.v | 37 |
1 files changed, 22 insertions, 15 deletions
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index c1f819412..d81589fc4 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -1,4 +1,4 @@ -Require Import Coq.Program.Tactics. +Require Import Coq.Program.Program. Variable A : Set. @@ -17,7 +17,7 @@ Require Import ProofIrrelevance. Goal forall n, forall v : vector (S n), exists v' : vector n, exists a : A, v = vcons a n v'. Proof. intros n H. - dependent induction H. + dependent induction H generalizing n. inversion H0 ; subst. rewrite (UIP_refl _ _ H0). simpl. @@ -52,20 +52,27 @@ Proof with simpl in * ; auto. dependent induction H generalizing G D. destruct D... - subst. - apply weak ; apply ax. - inversion H ; subst. - apply ax. - - induction D... - subst. - do 2 apply weak. - assumption. + subst. + apply weak ; apply ax. - apply weak. - apply IHterm. - inversion H0 ; subst ; reflexivity. + inversion H ; subst. + apply ax. + + destruct D... + subst. + do 2 apply weak. + assumption. - apply abs. + apply weak. + apply IHterm. + inversion H0 ; subst ; reflexivity. + + cut(term (snoc (app G0 D) tau'0) (arrow tau tau') -> term (app (snoc G0 tau'0) D) (arrow tau tau')). + intros. + apply H0. apply weak. + apply abs. + assumption. + + intros. Admitted. |