1 files changed, 0 insertions, 80 deletions
diff --git a/plugins/dp/test2.v b/plugins/dp/test2.v
deleted file mode 100644
index ce660052..00000000
--- a/plugins/dp/test2.v
+++ /dev/null
@@ -1,80 +0,0 @@
-Require Import ZArith.
-Require Import Classical.
-Require Import List.
-
-Open Scope list_scope.
-Open Scope Z_scope.
-
-Dp_debug.
-Dp_timeout 3.
-Require Export zenon.
-
-Definition neg (z:Z) : Z := match z with
-  | Z0 => Z0
-  | Zpos p => Zneg p
-  | Zneg p => Zpos p
-  end.
-
-Goal forall z, neg (neg z) = z.
-  Admitted.
-
-Open Scope nat_scope.
-Print plus.
-
-Goal forall x, x+0=x.
-  induction x; ergo.
-  (* simplify resoud le premier, pas le second *)
-  Admitted.
-
-Goal 1::2::3::nil = 1::2::(1+2)::nil.
-  zenon.
-  Admitted.
-
-Definition T := nat.
-Parameter fct : T -> nat.
-Goal fct O = O.
- Admitted.
-
-Fixpoint even (n:nat) : Prop :=
-  match n with
-  O => True
-  | S O => False
-  | S (S p) => even p
-  end.
-
-Goal even 4%nat.
-  try zenon.
-  Admitted.
-
-Definition p (A B:Set) (a:A) (b:B) : list (A*B) := cons (a,b) nil.
-
-Definition head :=
-fun (A : Set) (l : list A) =>
-match l with
-| nil => None (A:=A)
-| x :: _ => Some x
-end.
-
-Goal forall x, head _ (p _ _ 1 2) = Some x -> fst x = 1.
-
-Admitted.
-
-(*
-BUG avec head prédéfini : manque eta-expansion sur A:Set
-
-Goal forall x, head _ (p _ _ 1 2) = Some x -> fst x = 1.
-
-Print value.
-Print Some.
-
-zenon.
-*)
-
-Inductive IN (A:Set) : A -> list A -> Prop :=
-  | IN1 : forall x l, IN A x (x::l)
-  | IN2: forall x l, IN A x l -> forall y, IN A x (y::l).
-Arguments IN [A] _ _.
-
-Goal forall x, forall (l:list nat), IN x l -> IN x (1%nat::l).
-  zenon.
-Print In.