Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 0 insertions, 49 deletions

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