Various fixes in subtac, update some test cases.

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

3 files changed, 11 insertions, 49 deletions

diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v
index fb8b34eed..cc11c1513 100644
--- a/contrib/subtac/test/ListsTest.v
+++ b/contrib/subtac/test/ListsTest.v
@@ -36,7 +36,7 @@ Section app.
       | hd :: tl => hd :: (tl ++ l')
     end 
     where "x ++ y" := (app x y).
- 
+
   Next Obligation.
     intros.
     destruct_call app ; subtac_simpl.
@@ -70,13 +70,8 @@ Section Nth.
 
   Next Obligation.
   Proof.
-    intros.
-    simpl in * ; auto with arith.
-  Defined.
-
-  Next Obligation.
-  Proof.
-    intros.
     inversion l0.
   Defined.
 End Nth.
+
+Section 
diff --git a/contrib/subtac/test/Mutind.v b/contrib/subtac/test/Mutind.v
index 8a9bec52f..22ecdc94b 100644
--- a/contrib/subtac/test/Mutind.v
+++ b/contrib/subtac/test/Mutind.v
@@ -1,3 +1,4 @@
+Require Import List.
 Program Fixpoint f (a : nat) : { x : nat | x > 0 } := 
   match a with
   | 0 => 1
@@ -9,16 +10,6 @@ with g (a b : nat) { struct b } : { x : nat | x > 0 } :=
   | S b' => f b'
   end.
 
-Obligations of f.
-
-Obligation 1 of f.
-  simpl ; intros ; auto with arith.
-Defined.
-
-Obligation 1 of g.
-  simpl ; intros ; auto with arith.
-Defined.
-
 Check f.
 Check g.
 
diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v
index 809503aa2..e793e270d 100644
--- a/contrib/subtac/test/euclid.v
+++ b/contrib/subtac/test/euclid.v
@@ -1,6 +1,6 @@
-Notation "( x & y )" := (@existS _ _ x y) : core_scope.
-Unset Printing All.
+Require Import Coq.subtac.Utils.
 Require Import Coq.Arith.Compare_dec.
+Notation "( x & y )" := (existS _ x y) : core_scope.
   
 Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt}  :
   { q : nat & { r : nat | a = b * q + r /\ r < b } } :=
@@ -9,41 +9,17 @@ Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt}  :
   else (O & a).
 
 Require Import Omega.
-Obligations.
 
-Obligation 1.
-  intros.
-  simpl in * ; auto with arith.
-  omega.
-Defined.
+Obligations.
+Solve Obligations using subtac_simpl ; omega.
 
-Obligation 2 of euclid.
-  intros.
+Next Obligation.
   assert(x0 * S q' = x0 * q' + x0) by auto with arith ; omega.
 Defined.
 
-Obligation 4 of euclid.
-  exact Wf_nat.lt_wf.
-Defined.
-
-Obligation 3 of euclid.
-  intros.
-  omega.
-Qed.
-
-Eval cbv delta [euclid_obligation_1 euclid_obligation_2] in (euclid 0).
-
-Extraction Inline Fix_sub Fix_F_sub.  
-Extract Inductive sigT => "pair" [ "" ].
-Extract Inductive sumbool => "bool" [ "true" "false" ].
-Extraction le_lt_dec.
-Extraction euclid.
+Program Definition test_euclid : (prod nat nat) := let (q, r) := euclid 4 2 in (q, q).
 
+Eval lazy beta zeta delta iota in test_euclid.
 
 Program Definition testsig (a : nat) : { x : nat & { y : nat | x < y } } :=
   (a & S a).
-
-
-Solve Obligations using auto with zarith.
-
-Extraction testsig.