1 files changed, 0 insertions, 46 deletions
diff --git a/contrib/subtac/test/id.v b/contrib/subtac/test/id.v
deleted file mode 100644
index 9ae11088..00000000
--- a/contrib/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.