Commit f4328251 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Typo.

parent 5e950a10
......@@ -62,8 +62,7 @@ Qed.
Theorem FIX_format_satisfies_any :
satisfies_any FIX_format.
Proof.
pose (fexp (e : Z) := emin).
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta fexp _)).
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FIX_exp _)).
exact FIX_format_generic.
exact FIX_exp_correct.
Qed.
......
......@@ -96,8 +96,7 @@ Qed.
Theorem FLX_format_satisfies_any :
satisfies_any FLX_format.
Proof.
pose (fexp e := (e - prec)%Z).
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta fexp _)).
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLX_exp _)).
exact FLX_format_generic.
exact FLX_exp_correct.
Qed.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment