Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 0 insertions, 65 deletions

diff --git a/contrib/subtac/test/rec.v b/contrib/subtac/test/rec.v
deleted file mode 100644
index aaefd8cc..00000000
--- a/contrib/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.