Default tactic for solving goals.

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

1 files changed, 2 insertions, 8 deletions

diff --git a/contrib/subtac/test/take.v b/contrib/subtac/test/take.v
index 07f63a2ba8..f73507d2f5 100644
--- a/contrib/subtac/test/take.v
+++ b/contrib/subtac/test/take.v
@@ -1,14 +1,13 @@
-Variable A : Set.
 Require Import JMeq.
 Require Import List.
 Require Import Coq.subtac.Utils.
 
-Program Fixpoint take (l : list A) (n : nat | n <= length l) { struct l } : { l' : list A | length l' = n } :=
+Program Fixpoint take (A : Set) (l : list A) (n : nat | n <= length l) { struct l } : { l' : list A | length l' = n } :=
   match n with
   | 0 => nil
   | S p => 
     match l with
-    | cons hd tl => let rest := take tl p in cons hd rest
+    | cons hd tl => let rest := take A tl p in cons hd rest
     | nil => _
     end
   end.
@@ -22,18 +21,13 @@ Solve Obligations using (subtac_simpl ; subst ; auto with arith).
 Obligations.
 
 Obligation 3.
-  subtac_simpl.
   destruct_call take ; subtac_simpl ; subst ; auto.
 Defined.
 
 Obligation 4.
-  subtac_simpl.
   subst l x.
   simpl in l0.
   absurd (S p <= 0) ; omega.
 Defined.
 
-
-Print take.
-
 Extraction take.