start removing BaseSystem

1 files changed, 0 insertions, 18 deletions

diff --git a/src/Util/CaseUtil.v b/src/Util/CaseUtil.v
deleted file mode 100644
index 2d1ab6c58..000000000
--- a/src/Util/CaseUtil.v
+++ /dev/null
@@ -1,18 +0,0 @@
-Require Import Coq.Arith.Arith Coq.Arith.Max.
-
-Ltac case_max :=
-  match goal with [ |- context[max ?x ?y] ] =>
-      destruct (le_dec x y);
-      match goal with
-        | [ H : (?x <= ?y)%nat |- context[max ?x ?y] ] => rewrite max_r by
-          (exact H)
-        | [ H : ~ (?x <= ?y)%nat   |- context[max ?x ?y] ] => rewrite max_l by
-          (exact (le_Sn_le _ _ (not_le _ _ H)))
-      end
-  end.
-
-Lemma pull_app_if_sumbool {A B X Y} (b : sumbool X Y) (f g : A -> B) (x : A)
-  : (if b then f x else g x) = (if b then f else g) x.
-Proof.
-  destruct b; reflexivity.
-Qed.