3 files changed, 82 insertions, 4 deletions
diff --git a/contrib/subtac/test/Mutind.v b/contrib/subtac/test/Mutind.v
index ab200354c..0b40ef82a 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/measure.v b/contrib/subtac/test/measure.v
new file mode 100644
index 000000000..4764037d9
--- /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 000000000..49fec2b80
--- /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