5 files changed, 88 insertions, 10 deletions

diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v
index a29cd039..8429c267 100644
--- a/contrib/subtac/test/ListsTest.v
+++ b/contrib/subtac/test/ListsTest.v
@@ -5,12 +5,13 @@ Variable A : Set.
 
 Program Definition myhd : forall { l : list A | length l <> 0 }, A :=  
   fun l =>
-    match l with
+    match `l with
     | nil => _
     | hd :: tl => hd
     end.
 Proof.
-  destruct l ; simpl ; intro H ; rewrite <- H in n ; intuition.
+  destruct l ; simpl ; intro H.
+  rewrite H in n ; intuition.
 Defined.
 
 
@@ -24,7 +25,7 @@ Program Definition mytail : forall { l : list A | length l <> 0 }, list A :=
     | hd :: tl => tl
     end.
 Proof.
-destruct l ; simpl ; intro H ; rewrite <- H in n ; intuition.
+destruct l ; simpl ; intro H ; rewrite H in n ; intuition.
 Defined.
 
 Extraction mytail.
@@ -50,7 +51,6 @@ Program Fixpoint append (l : list A) (l' : list A) { struct l } :
  | nil => l'
  | hd :: tl => hd :: (append tl l')
  end.
-simpl.
 subst ; auto.
 simpl ; rewrite (subset_simpl (append tl0 l')).
 simpl ; subst.
diff --git a/contrib/subtac/test/Mutind.v b/contrib/subtac/test/Mutind.v
index ab200354..0b40ef82 100644
--- a/contrib/subtac/test/Mutind.v
+++ b/contrib/subtac/test/Mutind.v
@@ -1,7 +1,13 @@
-Fixpoint f (a : nat) : nat := match a with 0 => 0
-| S a' => g a a'
+Program Fixpoint f (a : nat) : nat := 
+  match a with
+  | 0 => 0
+  | S a' => g a a'
   end
 with g (a b : nat) { struct b } : nat := 
-  match b with 0 => 0
+  match b with
+  | 0 => 0
   | S b' => f b'
-  end.
\ No newline at end of file
+  end.
+
+Check f.
+Check g.
\ No newline at end of file
diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v
index 481b6708..ba5bdf23 100644
--- a/contrib/subtac/test/euclid.v
+++ b/contrib/subtac/test/euclid.v
@@ -12,8 +12,8 @@ reflexivity.
 Defined.
 
 Extraction testsig.
-Extraction sigS.
-Extract Inductive sigS => "" [ "" ].
+Extraction sig.
+Extract Inductive sig => "" [ "" ].
 Extraction testsig.
 
 Require Import Coq.Arith.Compare_dec.
diff --git a/contrib/subtac/test/measure.v b/contrib/subtac/test/measure.v
new file mode 100644
index 00000000..4764037d
--- /dev/null
+++ b/contrib/subtac/test/measure.v
@@ -0,0 +1,24 @@
+Notation "( x & y )" := (@existS _ _ x y) : core_scope.
+Unset Printing All.
+Require Import Coq.Arith.Compare_dec.
+
+Require Import Coq.subtac.Utils.
+
+Fixpoint size (a : nat) : nat :=
+  match a with
+  0 => 1
+  | S n => S (size n)
+  end.
+
+Program Fixpoint test_measure (a : nat) {measure a size}  : nat :=
+  match a with
+  | S (S n) => S (test_measure n)
+  | x => x
+  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/wf.v b/contrib/subtac/test/wf.v
new file mode 100644
index 00000000..49fec2b8
--- /dev/null
+++ b/contrib/subtac/test/wf.v
@@ -0,0 +1,48 @@
+Notation "( x & y )" := (@existS _ _ x y) : core_scope.
+Unset Printing All.
+Require Import Coq.Arith.Compare_dec.
+
+Require Import Coq.subtac.Utils.
+
+Ltac one_simpl_hyp :=
+ match goal with
+ | [H : (`exist _ _ _) = _ |- _] => simpl in H
+ | [H : _ = (`exist _ _ _) |- _] => simpl in H
+ | [H : (`exist _ _ _) < _ |- _] => simpl in H
+ | [H : _ < (`exist _ _ _) |- _] => simpl in H
+ | [H : (`exist _ _ _) <= _ |- _] => simpl in H
+ | [H : _ <= (`exist _ _ _) |- _] => simpl in H
+ | [H : (`exist _ _ _) > _ |- _] => simpl in H
+ | [H : _ > (`exist _ _ _) |- _] => simpl in H
+ | [H : (`exist _ _ _) >= _ |- _] => simpl in H
+ | [H : _ >= (`exist _ _ _) |- _] => simpl in H
+ end.
+
+Ltac one_simpl_subtac :=
+  destruct_exists ;
+  repeat one_simpl_hyp ; simpl.
+
+Ltac simpl_subtac :=  do 3 one_simpl_subtac ; simpl.
+
+Require Import Omega.
+Require Import Wf_nat.
+
+Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt}  :
+  { 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).
+destruct b ; simpl_subtac.
+omega.
+simpl_subtac.
+assert(x0 * S q' = x0 + x0 * q').
+rewrite <- mult_n_Sm.
+omega.
+rewrite H2 ; omega.
+simpl_subtac.
+split ; auto with arith.
+omega.
+apply lt_wf.
+Defined.
+
+Check euclid_evars_proof.
\ No newline at end of file