diff options
Diffstat (limited to 'lib/Coqlib.v')
-rw-r--r-- | lib/Coqlib.v | 7 |
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. |