fact: Definition loc_of_shr_record mrs := match mrs with | Build_shr_record _ false false => loc_Exact | Build_shr_record _ false true => loc_Inexact Lt | Build_shr_record _ true false => loc_Inexact Eq | Build_shr_record _ true true => loc_Inexact Gt end.
imports: ZArith FloatClass