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

2 files changed, 21 insertions, 17 deletions

diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v
index 3ceea173..05fc0803 100644
--- a/contrib/subtac/test/ListsTest.v
+++ b/contrib/subtac/test/ListsTest.v
@@ -1,5 +1,5 @@
 (* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
-Require Import Coq.subtac.Utils.
+Require Import Coq.Program.Program.
 Require Import List.
 
 Set Implicit Arguments.
@@ -7,7 +7,7 @@ Set Implicit Arguments.
 Section Accessors.
   Variable A : Set.
 
-  Program Definition myhd : forall { l : list A | length l <> 0 }, A :=  
+  Program Definition myhd : forall (l : list A | length l <> 0), A :=  
     fun l =>
       match l with
         | nil => !
@@ -39,7 +39,7 @@ Section app.
 
   Next Obligation.
     intros.
-    destruct_call app ; subtac_simpl.
+    destruct_call app ; program_simpl.
   Defined.
   
   Program Lemma app_id_l : forall l : list A, l = nil ++ l.
@@ -49,7 +49,7 @@ Section app.
   
   Program Lemma app_id_r : forall l : list A, l = l ++ nil.
   Proof.
-    induction l ; simpl ; auto.
+    induction l ; simpl in * ; auto. 
     rewrite <- IHl ; auto.
   Qed.
 
@@ -70,16 +70,24 @@ Section Nth.
 
   Next Obligation.
   Proof.
-    intros.
-    inversion H.
+    simpl in *. auto with arith. 
   Defined.
 
+  Next Obligation.
+  Proof.
+    inversion H.
+  Qed.
+
   Program Fixpoint nth' (l : list A) (n : nat | n < length l) { struct l } : A := 
     match l, n with
       | hd :: _, 0 => hd
       | _ :: tl, S n' => nth' tl n'
       | nil, _ => !
     end.
+  Next Obligation.
+  Proof.
+    simpl in *. auto with arith. 
+  Defined.
 
   Next Obligation.
   Proof.
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.