fact: Definition shr_record_of_loc m l := match l with | loc_Exact => Build_shr_record m false false | loc_Inexact Lt => Build_shr_record m false true | loc_Inexact Eq => Build_shr_record m true false | loc_Inexact Gt => Build_shr_record m true true end.
imports: ZArith FloatClass