we restored the scripts of \lambda\delta version 1

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/base_rewrite.v b/helm/coq-contribs/LAMBDA-TYPES/base_rewrite.v
deleted file mode 100644 (file)
index 68490ee..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/base_rewrite.v
+++ /dev/null
@@ -1,76 +0,0 @@
-(*#* #stop file *)
-
-Require Arith.
-
-      Tactic Definition Arith0 x :=
-         Replace (S x) with (plus (1) x); XAuto.
-
-      Tactic Definition Arith1 x :=
-         Replace x with (plus x (0)); [XAuto | Auto with arith].
-
-      Tactic Definition Arith1In H x :=
-         XReplaceIn H x '(plus x (0)).
-
-      Tactic Definition Arith2 x :=
-         Replace x with (plus (0) x); XAuto.
-
-      Tactic Definition Arith3 x :=
-         Replace (S x) with (S (plus (0) x)); XAuto.
-
-      Tactic Definition Arith3In H x :=
-         XReplaceIn H '(S x) '(S (plus (0) x)).
-
-      Tactic Definition Arith4 x y :=
-         Replace (S (plus x y)) with (plus (S x) y); XAuto.
-
-      Tactic Definition Arith4In H x y :=
-         XReplaceIn H '(S (plus x y)) '(plus (S x) y).
-
-      Tactic Definition Arith4c x y :=
-         Arith4 x y; Rewrite plus_sym.
-
-      Tactic Definition Arith5 x y :=
-         Replace (S (plus x y)) with (plus x (S y)); Auto with arith.
-
-      Tactic Definition Arith5In H x y :=
-         XReplaceIn H '(S (plus x y)) '(plus x (S y)); Auto with arith.
-
-      Tactic Definition Arith5' x y :=
-         Replace (plus x (S y)) with (S (plus x y)); Auto with arith.
-
-      Tactic Definition Arith5'In H x y :=
-         XReplaceIn H '(plus x (S y)) '(S (plus x y)); Auto with arith.
-
-      Tactic Definition Arith5'c x y :=
-         Arith5' x y; Rewrite plus_sym.
-
-      Tactic Definition Arith6In H x y :=
-         XReplaceIn H '(plus x (S y)) '(plus (1) (plus x y));
-         [ Idtac | Simpl; Auto with arith ].
-
-      Tactic Definition Arith7 x :=
-         Replace (S x) with (plus x (1));
-         [ Idtac | Rewrite plus_sym; Auto with arith ].
-
-      Tactic Definition Arith7In H x :=
-         XReplaceIn H '(S x) '(plus x (1)) ;
-         [ Idtac | Rewrite plus_sym; Auto with arith ].
-
-      Tactic Definition Arith7' x :=
-         Replace (plus x (1)) with (S x);
-         [ Idtac | Rewrite plus_sym; Auto with arith ].
-
-      Tactic Definition Arith8 x y :=
-         Replace x with (plus y (minus x y));
-         [ Idtac | Auto with arith ].
-
-      Tactic Definition Arith8' x y :=
-         Replace (plus y (minus x y)) with x;
-         [ Idtac | Auto with arith ].
-
-      Tactic Definition Arith9'In H x :=
-         XReplaceIn H '(S (plus x (0))) '(S x).
-
-      Tactic Definition Arith10 x :=
-         Replace x with (minus (S x) (1));
-         [ Idtac | Simpl; Rewrite <- minus_n_O; Auto with arith ].