Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg

1 files changed, 7 insertions, 11 deletions

diff --git a/contrib/subtac/test/take.v b/contrib/subtac/test/take.v
index 87ab47d6..2e17959c 100644
--- a/contrib/subtac/test/take.v
+++ b/contrib/subtac/test/take.v
@@ -1,9 +1,12 @@
 (* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
 Require Import JMeq.
 Require Import List.
-Require Import Coq.subtac.Utils.
+Require Import Program.
 
 Set Implicit Arguments.
+Obligations Tactic := idtac.
+
+Print cons.
 
 Program Fixpoint take (A : Set) (l : list A) (n : nat | n <= length l) { struct l } : { l' : list A | length l' = n } :=
   match n with
@@ -16,21 +19,14 @@ Program Fixpoint take (A : Set) (l : list A) (n : nat | n <= length l) { struct
   end.
 
 Require Import Omega.
-
+Solve All Obligations.
 Next Obligation.
-  intros.
-  simpl in l0.
-  apply le_S_n ; exact l0.
-Defined.
-
-Next Obligation.
-  intros.
-  destruct_call take ; subtac_simpl.
+  destruct_call take ; program_simpl.
 Defined.
 
 Next Obligation.
   intros.
-  inversion l0.
+  inversion H.
 Defined.