diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-06-26 14:09:33 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-09-06 15:58:30 +0200 |
| commit | 7dca5905e7921b72634c31ae8de1bd08b3ff2e2e (patch) | |
| tree | 965aebe90748c9bd3cd036e4d656aeb3bb4b0357 /lib/Coqlib.v | |
| parent | 0236781c3ff798b60c5c8171a0f9b6cd569f7995 (diff) | |
| download | compcert-kvx-7dca5905e7921b72634c31ae8de1bd08b3ff2e2e.tar.gz compcert-kvx-7dca5905e7921b72634c31ae8de1bd08b3ff2e2e.zip | |
Machblock: some cleaning
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. |