diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-05-24 15:06:18 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-09-06 15:58:30 +0200 |
| commit | 0236781c3ff798b60c5c8171a0f9b6cd569f7995 (patch) | |
| tree | 117e80f627ac331c066db3140a14040603118424 /lib/Coqlib.v | |
| parent | 265fdd4f703b0310fbcf5ad448c29dc34f7ff33a (diff) | |
| download | compcert-kvx-0236781c3ff798b60c5c8171a0f9b6cd569f7995.tar.gz compcert-kvx-0236781c3ff798b60c5c8171a0f9b6cd569f7995.zip | |
Machblock: Mach language with basic blocks
Diffstat (limited to 'lib/Coqlib.v')
| -rw-r--r-- | lib/Coqlib.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 3fe1ea2e..86bfa248 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -90,6 +90,13 @@ 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. |