Subtac: work on cases.

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

1 files changed, 11 insertions, 11 deletions

diff --git a/contrib/subtac/test/take.v b/contrib/subtac/test/take.v
index fbb1727eae..968ab3ad77 100644
--- a/contrib/subtac/test/take.v
+++ b/contrib/subtac/test/take.v
@@ -1,20 +1,19 @@
 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 } :=
   match n with
   | 0 => nil
-  | S n => 
+  | S p => 
     match l with
-    | cons hd tl => let rest := take tl n in cons hd rest
-    | _ => _
+    | cons hd tl => let rest := take tl p in cons hd rest
+    | nil => _
     end
   end.
-  
-Require Import Omega.
 
+Require Import Omega.
 
 Obligations.
 
@@ -22,18 +21,19 @@ Solve Obligations using (subtac_simpl ; subst ; auto with arith).
 
 Obligations.
 
-Obligation 2.
+Obligation 3.
   subtac_simpl.
-  subst l x.
-  simpl in l0.
-  absurd (S n0 <= 0) ; omega.
+  destruct_call take ; subtac_simpl ; subst ; auto.
 Defined.
 
 Obligation 4.
   subtac_simpl.
-  destruct_call take ; subtac_simpl ; subst ; auto.
+  subst l x.
+  simpl in l0.
+  absurd (S p <= 0) ; omega.
 Defined.
 
+
 Print take.
 
 Extraction take.