From 640a6d2f48ba07b51bcabc4235eaa4a497f4c263 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 2 Jan 2008 13:26:08 +0000
Subject: 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
---
 test-suite/bugs/closed/shouldsucceed/1411.v |  2 +-
 test-suite/success/dependentind.v           | 37 +++++++++++++++++------------
 2 files changed, 23 insertions(+), 16 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/shouldsucceed/1411.v b/test-suite/bugs/closed/shouldsucceed/1411.v
index 11eb69b5d3..bb475bdc2a 100644
--- a/test-suite/bugs/closed/shouldsucceed/1411.v
+++ b/test-suite/bugs/closed/shouldsucceed/1411.v
@@ -18,7 +18,7 @@ intros.
 destruct H.
 Defined.
 
-Program Fixpoint fetch t p (x:Exact t p) {struct x} :=
+Program Fixpoint fetch t p (x:Exact t p) {struct t} :=
    match t, p with
    | No p' , nil      => p'
    | No p' , _::_     => unreachable nat _
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index c1f8194124..d81589fc47 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.
-- 
cgit v1.2.3