we restored the scripts of \lambda\delta version 1

[helm.git] / helm / coq-contribs / LAMBDA-TYPES / base_tactics.v

diff --git a/helm/coq-contribs/LAMBDA-TYPES/base_tactics.v b/helm/coq-contribs/LAMBDA-TYPES/base_tactics.v
deleted file mode 100644 (file)
index daa6fac..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/base_tactics.v
+++ /dev/null
@@ -1,45 +0,0 @@
-(*#* #stop file *)
-
-      Tactic Definition XAuto := Auto with ltlc.
-
-      Tactic Definition XEAuto := EAuto with ltlc.
-
-      Tactic Definition XDEAuto d := EAuto d with ltlc.
-
-      Tactic Definition XElimUsing e v :=
-         Try Intros until v; Elim v using e; Try Clear v.
-
-      Tactic Definition XElim v := Try Intros until v; Elim v; Try Clear v.
-
-      Tactic Definition XCase v := Try Intros until v; Case v; Try Clear v.
-
-      Tactic Definition XReplaceIn Z0 y1 y2 :=
-         Cut y1=y2; [ Intros Z; Rewrite Z in Z0; Clear Z | XAuto ].
-
-      Theorem insert_eq: (S:Set; x:S; P:S->Prop; G:Prop)
-                         ((y:S) (P y) -> y = x -> G) -> (P x) -> G.
-      EAuto. Qed.
-
-      Tactic Definition InsertEq H y :=
-         Pattern 1 y in H; Match Context With [ _: (?1 y) |- ? ] ->
-         Apply insert_eq with x:=y P:=?1;
-         [ Clear H; Intros until 1 | Pattern y; Apply H ].
-
-      Theorem unintro : (A:Set; a:A; P:A->Prop) ((x:A) (P x)) -> (P a).
-      Auto.
-      Qed.
-
-      Tactic Definition UnIntro Last H :=
-         Move H after Last;
-         Match Context With [ y: ?1 |- ?2 ] ->
-            Apply (unintro ?1 y); Clear y.
-
-      Tactic Definition NonLinear :=
-         Match Context With
-            [ H: ?1 |- ? ] -> Cut ?1; [ Intros | XAuto ].
-
-      Tactic Definition XRewrite x :=
-         Match Context With
-            | [ H0: x = ? |- ? ] -> Try Rewrite H0
-            | [ H0: ? = x |- ? ] -> Try Rewrite <- H0
-            | _                  -> Idtac.