aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Coqlib.v
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Coqlib.v')
-rw-r--r--lib/Coqlib.v7
1 files changed, 0 insertions, 7 deletions
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 86bfa248..3fe1ea2e 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -90,13 +90,6 @@ Ltac exploit x :=
|| refine (modusponens _ _ (x _ _) _)
|| refine (modusponens _ _ (x _) _).
-Ltac totologize H :=
- match type of H with
- | ( ?id = _ ) =>
- let Hassert := fresh "Htoto" in (
- assert (id = id) as Hassert; auto; rewrite H in Hassert at 2; simpl in Hassert; rewrite H in Hassert)
- end.
-
(** * Definitions and theorems over the type [positive] *)
Definition peq: forall (x y: positive), {x = y} + {x <> y} := Pos.eq_dec.