5 files changed, 61 insertions, 23 deletions

diff --git a/contrib/subtac/test/ListDep.v b/contrib/subtac/test/ListDep.v
index 97cef9a5..da612c43 100644
--- a/contrib/subtac/test/ListDep.v
+++ b/contrib/subtac/test/ListDep.v
@@ -1,6 +1,6 @@
 (* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
 Require Import List.
-Require Import Coq.subtac.Utils.
+Require Import Coq.Program.Program.
 
 Set Implicit Arguments.
 
@@ -23,13 +23,13 @@ Section Map_DependentRecursor.
   Variable f : { x : U | In x l } -> V.
 
   Obligations Tactic := unfold sub_list in * ; 
-    subtac_simpl ; intuition.
+    program_simpl ; intuition.
 
   Program Fixpoint map_rec ( l' : list U | sub_list l' l )
     { measure length l' } : { r : list V | length r = length l' } :=
     match l' with
-    nil => nil
-    | cons x tl => let tl' := map_rec tl in
+      | nil => nil
+      | cons x tl => let tl' := map_rec tl in
 	f x :: tl'
     end.
     
diff --git a/contrib/subtac/test/Mutind.v b/contrib/subtac/test/Mutind.v
index 0b40ef82..ac49ca96 100644
--- a/contrib/subtac/test/Mutind.v
+++ b/contrib/subtac/test/Mutind.v
@@ -1,13 +1,20 @@
-Program Fixpoint f (a : nat) : nat := 
+Require Import List.
+
+Program Fixpoint f a : { x : nat | x > 0 } := 
   match a with
-  | 0 => 0
+  | 0 => 1
   | S a' => g a a'
   end
-with g (a b : nat) { struct b } : nat := 
+with g a b : { x : nat | x > 0 } := 
   match b with
-  | 0 => 0
+  | 0 => 1
   | S b' => f b'
   end.
 
 Check f.
-Check g.
\ No newline at end of file
+Check g.
+
+
+
+
+
diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v
index a5a8b85f..501aa798 100644
--- a/contrib/subtac/test/euclid.v
+++ b/contrib/subtac/test/euclid.v
@@ -1,20 +1,17 @@
-Require Import Coq.subtac.Utils.
+Require Import Coq.Program.Program.
 Require Import Coq.Arith.Compare_dec.
 Notation "( x & y )" := (existS _ x y) : core_scope.
   
+Require Import Omega.
+
 Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf lt a}  :
   { q : nat & { r : nat | a = b * q + r /\ r < b } } :=
   if le_lt_dec b a then let (q', r) := euclid (a - b) b in 
   (S q' & r)
   else (O & a).
 
-Require Import Omega.
-
-Obligations.
-Solve Obligations using subtac_simpl ; omega.
-
 Next Obligation.
-  assert(x0 * S q' = x0 * q' + x0) by auto with arith ; omega.
+  assert(b * S q' = b * q' + b) by auto with arith ; omega.
 Defined.
 
 Program Definition test_euclid : (prod nat nat) := let (q, r) := euclid 4 2 in (q, q).
diff --git a/contrib/subtac/test/measure.v b/contrib/subtac/test/measure.v
index 4764037d..4f938f4f 100644
--- a/contrib/subtac/test/measure.v
+++ b/contrib/subtac/test/measure.v
@@ -2,7 +2,7 @@ Notation "( x & y )" := (@existS _ _ x y) : core_scope.
 Unset Printing All.
 Require Import Coq.Arith.Compare_dec.
 
-Require Import Coq.subtac.Utils.
+Require Import Coq.Program.Program.
 
 Fixpoint size (a : nat) : nat :=
   match a with
@@ -10,15 +10,11 @@ Fixpoint size (a : nat) : nat :=
   | S n => S (size n)
   end.
 
-Program Fixpoint test_measure (a : nat) {measure a size}  : nat :=
+Program Fixpoint test_measure (a : nat) {measure size a}  : nat :=
   match a with
   | S (S n) => S (test_measure n)
-  | x => x
+  | 0 | S 0 => a
   end.
-subst.
-unfold n0.
-auto with arith.
-Qed.
 
 Check test_measure.
 Print test_measure.
\ No newline at end of file
diff --git a/contrib/subtac/test/take.v b/contrib/subtac/test/take.v
new file mode 100644
index 00000000..87ab47d6
--- /dev/null
+++ b/contrib/subtac/test/take.v
@@ -0,0 +1,38 @@
+(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
+Require Import JMeq.
+Require Import List.
+Require Import Coq.subtac.Utils.
+
+Set Implicit Arguments.
+
+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
+    | nil => !
+    end
+  end.
+
+Require Import Omega.
+
+Next Obligation.
+  intros.
+  simpl in l0.
+  apply le_S_n ; exact l0.
+Defined.
+
+Next Obligation.
+  intros.
+  destruct_call take ; subtac_simpl.
+Defined.
+
+Next Obligation.
+  intros.
+  inversion l0.
+Defined.
+
+
+
+