diff options
Diffstat (limited to 'backend/Constprop.v')
| -rw-r--r-- | backend/Constprop.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Constprop.v b/backend/Constprop.v index 8fa0691..2f3123f 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -49,7 +49,7 @@ Module Approx <: SEMILATTICE_WITH_TOP. apply Int.eq_dec. apply ident_eq. apply Int.eq_dec. - Qed. + Defined. Definition beq (x y: t) := if eq_dec x y then true else false. Lemma beq_correct: forall x y, beq x y = true -> x = y. Proof. |