10 files changed, 0 insertions, 421 deletions

diff --git a/plugins/subtac/test/ListDep.v b/plugins/subtac/test/ListDep.v
deleted file mode 100644
index e3dbd127..00000000
--- a/plugins/subtac/test/ListDep.v
+++ /dev/null
@@ -1,49 +0,0 @@
-(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
-Require Import List.
-Require Import Coq.Program.Program.
-
-Set Implicit Arguments.
-
-Definition sub_list (A : Set) (l' l : list A) := (forall v, In v l' -> In v l) /\ length l' <= length l.
-
-Lemma sub_list_tl : forall A : Set, forall x (l l' : list A), sub_list (x :: l) l' -> sub_list l l'.
-Proof.
-  intros.
-  inversion H.
-  split.
-  intros.
-  apply H0.
-  auto with datatypes.
-  auto with arith.
-Qed.
-
-Section Map_DependentRecursor.
-  Variable U V : Set.
-  Variable l : list U.
-  Variable f : { x : U | In x l } -> V.
-
-  Obligations Tactic := unfold sub_list in * ;
-    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
-	f x :: tl'
-    end.
-
-  Next Obligation.
-    destruct_call map_rec.
-    simpl in *.
-    subst l'.
-    simpl ; auto with arith.
-  Qed.
-
-  Program Definition map : list V := map_rec l.
-
-End Map_DependentRecursor.
-
-Extraction map.
-Extraction map_rec.
-
diff --git a/plugins/subtac/test/ListsTest.v b/plugins/subtac/test/ListsTest.v
deleted file mode 100644
index 2cea0841..00000000
--- a/plugins/subtac/test/ListsTest.v
+++ /dev/null
@@ -1,99 +0,0 @@
-(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
-Require Import Coq.Program.Program.
-Require Import List.
-
-Set Implicit Arguments.
-
-Section Accessors.
-  Variable A : Set.
-
-  Program Definition myhd : forall (l : list A | length l <> 0), A :=
-    fun l =>
-      match l with
-        | nil => !
-        | hd :: tl => hd
-      end.
-
-  Program Definition mytail (l : list A | length l <> 0) : list A :=
-    match l with
-      | nil => !
-      | hd :: tl => tl
-    end.
-End Accessors.
-
-Program Definition test_hd : nat := myhd (cons 1 nil).
-
-(*Eval compute in test_hd*)
-(*Program Definition test_tail : list A := mytail nil.*)
-
-Section app.
-  Variable A : Set.
-
-  Program Fixpoint app (l : list A) (l' : list A) { struct l } :
-    { r : list A | length r = length l + length l' } :=
-    match l with
-      | nil => l'
-      | hd :: tl => hd :: (tl ++ l')
-    end
-    where "x ++ y" := (app x y).
-
-  Next Obligation.
-    intros.
-    destruct_call app ; program_simpl.
-  Defined.
-
-  Program Lemma app_id_l : forall l : list A, l = nil ++ l.
-  Proof.
-    simpl ; auto.
-  Qed.
-
-  Program Lemma app_id_r : forall l : list A, l = l ++ nil.
-  Proof.
-    induction l ; simpl in * ; auto.
-    rewrite <- IHl ; auto.
-  Qed.
-
-End app.
-
-Extraction app.
-
-Section Nth.
-
-  Variable A : Set.
-
-  Program Fixpoint nth (l : list A) (n : nat | n < length l) { struct l } : A :=
-    match n, l with
-      | 0, hd :: _ => hd
-      | S n', _ :: tl => nth tl n'
-      | _, nil => !
-    end.
-
-  Next Obligation.
-  Proof.
-    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.
-    intros.
-    inversion H.
-  Defined.
-
-End Nth.
-
diff --git a/plugins/subtac/test/Mutind.v b/plugins/subtac/test/Mutind.v
deleted file mode 100644
index 01e2d75f..00000000
--- a/plugins/subtac/test/Mutind.v
+++ /dev/null
@@ -1,20 +0,0 @@
-Require Import List.
-
-Program Fixpoint f a : { x : nat | x > 0 } :=
-  match a with
-  | 0 => 1
-  | S a' => g a a'
-  end
-with g a b : { x : nat | x > 0 } :=
-  match b with
-  | 0 => 1
-  | S b' => f b'
-  end.
-
-Check f.
-Check g.
-
-
-
-
-
diff --git a/plugins/subtac/test/Test1.v b/plugins/subtac/test/Test1.v
deleted file mode 100644
index 7e0755d5..00000000
--- a/plugins/subtac/test/Test1.v
+++ /dev/null
@@ -1,16 +0,0 @@
-Program Definition test (a b : nat) : { x : nat | x = a + b } :=
-  ((a + b) : { x : nat | x = a + b }).
-Proof.
-intros.
-reflexivity.
-Qed.
-
-Print test.
-
-Require Import List.
-
-Program hd_opt (l : list nat) : { x : nat | x <> 0 } :=
-  match l with
-    nil => 1
-    | a :: l => a
-  end.
diff --git a/plugins/subtac/test/euclid.v b/plugins/subtac/test/euclid.v
deleted file mode 100644
index 97c3d941..00000000
--- a/plugins/subtac/test/euclid.v
+++ /dev/null
@@ -1,24 +0,0 @@
-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).
-
-Next Obligation.
-  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).
-
-Eval lazy beta zeta delta iota in test_euclid.
-
-Program Definition testsig (a : nat) : { x : nat & { y : nat | x < y } } :=
-  (a & S a).
-
-Check testsig.
diff --git a/plugins/subtac/test/id.v b/plugins/subtac/test/id.v
deleted file mode 100644
index 9ae11088..00000000
--- a/plugins/subtac/test/id.v
+++ /dev/null
@@ -1,46 +0,0 @@
-Require Coq.Arith.Arith.
-
-Require Import Coq.subtac.Utils.
-Program Fixpoint id (n : nat) : { x : nat | x = n } :=
-  match n with
-  | O => O
-  | S p => S (id p)
-  end.
-intros ; auto.
-
-pose (subset_simpl (id p)).
-simpl in e.
-unfold p0.
-rewrite e.
-auto.
-Defined.
-
-Check id.
-Print id.
-Extraction id.
-
-Axiom le_gt_dec : forall n m, { n <= m } + { n > m }.
-Require Import Omega.
-
-Program Fixpoint id_if (n : nat) { wf n lt }: { x : nat | x = n } :=
-  if le_gt_dec n 0 then 0
-  else S (id_if (pred n)).
-intros.
-auto with arith.
-intros.
-pose (subset_simpl (id_if (pred n))).
-simpl in e.
-rewrite e.
-induction n ; auto with arith.
-Defined.
-
-Print id_if_instance.
-Extraction id_if_instance.
-
-Notation "( x & y )" := (@existS _ _ x y) : core_scope.
-
-Program Definition testsig ( a : nat ) : { x : nat & { y : nat | x = y }} :=
-  (a & a).
-intros.
-auto.
-Qed.
diff --git a/plugins/subtac/test/measure.v b/plugins/subtac/test/measure.v
deleted file mode 100644
index 4f938f4f..00000000
--- a/plugins/subtac/test/measure.v
+++ /dev/null
@@ -1,20 +0,0 @@
-Notation "( x & y )" := (@existS _ _ x y) : core_scope.
-Unset Printing All.
-Require Import Coq.Arith.Compare_dec.
-
-Require Import Coq.Program.Program.
-
-Fixpoint size (a : nat) : nat :=
-  match a with
-  0 => 1
-  | S n => S (size n)
-  end.
-
-Program Fixpoint test_measure (a : nat) {measure size a}  : nat :=
-  match a with
-  | S (S n) => S (test_measure n)
-  | 0 | S 0 => a
-  end.
-
-Check test_measure.
-Print test_measure.
\ No newline at end of file
diff --git a/plugins/subtac/test/rec.v b/plugins/subtac/test/rec.v
deleted file mode 100644
index aaefd8cc..00000000
--- a/plugins/subtac/test/rec.v
+++ /dev/null
@@ -1,65 +0,0 @@
-Require Import Coq.Arith.Arith.
-Require Import Lt.
-Require Import Omega.
-
-Axiom lt_ge_dec : forall x y : nat, { x < y } + { x >= y }.
-(*Proof.
-  intros.
-  elim (le_lt_dec y x) ; intros ; auto with arith.
-Defined.
-*)
-Require Import Coq.subtac.FixSub.
-Require Import Wf_nat.
-
-Lemma preda_lt_a : forall a, 0 < a -> pred a < a.
-auto with arith.
-Qed.
-
-Program Fixpoint id_struct (a : nat) : nat :=
-  match a with
-  0 => 0
-  | S n => S (id_struct n)
-  end.
-
-Check struct_rec.
-
-  if (lt_ge_dec O a)
-  then S (wfrec (pred a))
-  else O.
-
-Program Fixpoint wfrec (a : nat) { wf a lt } : nat :=
-  if (lt_ge_dec O a)
-  then S (wfrec (pred a))
-  else O.
-intros.
-apply preda_lt_a ; auto.
-
-Defined.
-
-Extraction wfrec.
-Extraction Inline proj1_sig.
-Extract Inductive bool => "bool" [ "true" "false" ].
-Extract Inductive sumbool => "bool" [ "true" "false" ].
-Extract Inlined Constant lt_ge_dec => "<".
-
-Extraction wfrec.
-Extraction Inline lt_ge_dec le_lt_dec.
-Extraction wfrec.
-
-
-Program Fixpoint structrec (a : nat) { wf a lt } : nat :=
-  match a with
-   S n => S (structrec n)
-   | 0 => 0
-   end.
-intros.
-unfold n0.
-omega.
-Defined.
-
-Print structrec.
-Extraction structrec.
-Extraction structrec.
-
-Definition structrec_fun (a : nat) : nat := structrec a (lt_wf a).
-Print structrec_fun.
diff --git a/plugins/subtac/test/take.v b/plugins/subtac/test/take.v
deleted file mode 100644
index 90ae8bae..00000000
--- a/plugins/subtac/test/take.v
+++ /dev/null
@@ -1,34 +0,0 @@
-(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
-Require Import JMeq.
-Require Import List.
-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
-  | 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.
-Solve All Obligations.
-Next Obligation.
-  destruct_call take ; program_simpl.
-Defined.
-
-Next Obligation.
-  intros.
-  inversion H.
-Defined.
-
-
-
-
diff --git a/plugins/subtac/test/wf.v b/plugins/subtac/test/wf.v
deleted file mode 100644
index 5ccc154a..00000000
--- a/plugins/subtac/test/wf.v
+++ /dev/null
@@ -1,48 +0,0 @@
-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