Commit d38b023f authored by root's avatar root

update

parent 905dcb26
......@@ -38,6 +38,7 @@ HasMeta cic:/Flocq/Calc?Bracket http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Flocq/Calc?Bracket cic:/Coq/ZArith?Zdiv
Includes cic:/Flocq/Calc?Bracket cic:/Coq/setoid_ring?ZArithRing
Includes cic:/Flocq/Calc?Bracket cic:/Coq/ZArith?BinInt
Includes cic:/Flocq/Calc?Bracket cic:/Flocq/Core?Zaux
Includes cic:/Flocq/Calc?Bracket cic:/Coq/ZArith?Zbool
Includes cic:/Flocq/Calc?Bracket cic:/Coq/Classes?Morphisms_Prop
Includes cic:/Flocq/Calc?Bracket cic:/Coq/ZArith?Zorder
......@@ -60,6 +61,7 @@ Includes cic:/Flocq/Calc?Bracket cic:/Coq/Init?Logic
Includes cic:/Flocq/Calc?Bracket cic:/Coq/Numbers?BinNums
Includes cic:/Flocq/Calc?Bracket cic:/Coq/Init?Datatypes
Includes cic:/Flocq/Calc?Bracket cic:/Coq/Reals?Rdefinitions
Includes cic:/Flocq/Calc?Bracket cic:/Flocq/Core?Float_prop
Includes cic:/Flocq/Calc?Bracket cic:/Flocq/Core?Defs
Includes cic:/Flocq/Calc?Bracket http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/Flocq/Calc?Bracket cic:/Flocq/Calc?Bracket?Fcalc_bracket
......
......@@ -26,7 +26,11 @@ Includes cic:/Flocq/Calc?Div cic:/Coq/Reals?Rdefinitions
Includes cic:/Flocq/Calc?Div cic:/Coq/Init?Logic
Includes cic:/Flocq/Calc?Div cic:/Coq/ZArith?BinInt/Z
Includes cic:/Flocq/Calc?Div cic:/Coq/Numbers?BinNums
Includes cic:/Flocq/Calc?Div cic:/Flocq/Core?Zaux
Includes cic:/Flocq/Calc?Div cic:/Flocq/Calc?Bracket
Includes cic:/Flocq/Calc?Div cic:/Flocq/Core?Digits
Includes cic:/Flocq/Calc?Div cic:/Flocq/Core?Float_prop
Includes cic:/Flocq/Calc?Div cic:/Flocq/Core?Generic_fmt
Includes cic:/Flocq/Calc?Div cic:/Flocq/Core?Defs
Includes cic:/Flocq/Calc?Div http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/Flocq/Calc?Div cic:/Flocq/Calc?Div?Fcalc_div
......
......@@ -31,6 +31,8 @@ Includes cic:/Flocq/Calc?Operations cic:/Coq/Init?Logic
Includes cic:/Flocq/Calc?Operations cic:/Coq/ZArith?BinInt/Z
Includes cic:/Flocq/Calc?Operations cic:/Coq/Numbers?BinNums
Includes cic:/Flocq/Calc?Operations cic:/Coq/Init?Datatypes
Includes cic:/Flocq/Calc?Operations cic:/Flocq/Core?Zaux
Includes cic:/Flocq/Calc?Operations cic:/Flocq/Core?Float_prop
Includes cic:/Flocq/Calc?Operations cic:/Flocq/Core?Defs
Includes cic:/Flocq/Calc?Operations http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/Flocq/Calc?Operations cic:/Flocq/Calc?Operations?Float_ops
......
......@@ -79,6 +79,7 @@ dataconstructor cic:/Flocq/Calc?Round?truncate_FIX
dataconstructor cic:/Flocq/Calc?Round?truncate_FIX_correct
theory cic:/Flocq/Calc?Round
HasMeta cic:/Flocq/Calc?Round http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Flocq/Calc?Round cic:/Flocq/Core?FIX
Includes cic:/Flocq/Calc?Round cic:/Coq/ZArith?Zbool
Includes cic:/Flocq/Calc?Round cic:/Coq/Classes?Morphisms_Prop
Includes cic:/Flocq/Calc?Round cic:/Coq/ZArith?Zdiv
......@@ -106,10 +107,13 @@ Includes cic:/Flocq/Calc?Round cic:/Coq/ZArith?Zorder
Includes cic:/Flocq/Calc?Round cic:/Coq/ZArith?BinInt/Z
Includes cic:/Flocq/Calc?Round cic:/Coq/Init?Logic
Includes cic:/Flocq/Calc?Round cic:/Coq/Reals?Rdefinitions
Includes cic:/Flocq/Calc?Round cic:/Flocq/Core?Generic_fmt
Includes cic:/Flocq/Calc?Round cic:/Coq/Numbers?BinNums
Includes cic:/Flocq/Calc?Round cic:/Flocq/Core?Zaux
Includes cic:/Flocq/Calc?Round cic:/Flocq/Calc?Bracket
Includes cic:/Flocq/Calc?Round cic:/Flocq/Core?Float_prop
Includes cic:/Flocq/Calc?Round cic:/Flocq/Core?Digits
Includes cic:/Flocq/Calc?Round cic:/Flocq/Core?Core
Includes cic:/Flocq/Calc?Round http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/Flocq/Calc?Round cic:/Flocq/Calc?Round?Fcalc_round
deriveddeclaration cic:/Flocq/Calc?Round?Fcalc_round
Declares cic:/Flocq/Calc?Round cic:/Flocq/Calc?Round?cexp_inbetween_float
......
......@@ -24,7 +24,11 @@ Includes cic:/Flocq/Calc?Sqrt cic:/Coq/Reals?R_sqrt
Includes cic:/Flocq/Calc?Sqrt cic:/Coq/Init?Logic
Includes cic:/Flocq/Calc?Sqrt cic:/Coq/ZArith?BinInt/Z
Includes cic:/Flocq/Calc?Sqrt cic:/Coq/Numbers?BinNums
Includes cic:/Flocq/Calc?Sqrt cic:/Flocq/Core?Zaux
Includes cic:/Flocq/Calc?Sqrt cic:/Flocq/Calc?Bracket
Includes cic:/Flocq/Calc?Sqrt cic:/Flocq/Core?Float_prop
Includes cic:/Flocq/Calc?Sqrt cic:/Flocq/Core?Generic_fmt
Includes cic:/Flocq/Calc?Sqrt cic:/Flocq/Core?Digits
Includes cic:/Flocq/Calc?Sqrt cic:/Flocq/Core?Defs
Includes cic:/Flocq/Calc?Sqrt http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/Flocq/Calc?Sqrt cic:/Flocq/Calc?Sqrt?Fcalc_sqrt
......
theory cic:/Flocq/Core?Core
HasMeta cic:/Flocq/Core?Core http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Flocq/Core?Core cic:/Flocq/Core?Defs
Includes cic:/Flocq/Core?Core cic:/Flocq/Core?Ulp
Includes cic:/Flocq/Core?Core cic:/Flocq/Core?FLT
Includes cic:/Flocq/Core?Core cic:/Flocq/Core?FLX
Includes cic:/Flocq/Core?Core cic:/Flocq/Core?FIX
Includes cic:/Flocq/Core?Core cic:/Flocq/Core?Round_NE
Includes cic:/Flocq/Core?Core cic:/Flocq/Core?Generic_fmt
Includes cic:/Flocq/Core?Core cic:/Flocq/Core?Round_pred
Includes cic:/Flocq/Core?Core cic:/Flocq/Core?Float_prop
Includes cic:/Flocq/Core?Core http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Flocq/Core?Core cic:/Flocq/Core?Defs
......@@ -12,6 +12,11 @@ dataconstructor cic:/Flocq/Core?Defs?Rnd_NG_pt
dataconstructor cic:/Flocq/Core?Defs?Rnd_NA_pt
theory cic:/Flocq/Core?Defs
HasMeta cic:/Flocq/Core?Defs http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Flocq/Core?Defs cic:/Coq/Reals?Rbasic_fun
Includes cic:/Flocq/Core?Defs cic:/Coq/Init?Logic
Includes cic:/Flocq/Core?Defs cic:/Coq/Reals?Rdefinitions
Includes cic:/Flocq/Core?Defs cic:/Coq/Numbers?BinNums
Includes cic:/Flocq/Core?Defs cic:/Flocq/Core?Zaux
Includes cic:/Flocq/Core?Defs http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/Flocq/Core?Defs cic:/Flocq/Core?Defs?Def
deriveddeclaration cic:/Flocq/Core?Defs?Def
......
This diff is collapsed.
......@@ -7,18 +7,13 @@ dataconstructor cic:/Flocq/Core?FIX?FIX_exp_monotone
dataconstructor cic:/Flocq/Core?FIX?ulp_FIX
theory cic:/Flocq/Core?FIX
HasMeta cic:/Flocq/Core?FIX http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Flocq/Core?FIX cic:/Coq/ZArith?auxiliary
Includes cic:/Flocq/Core?FIX cic:/Coq/omega?OmegaLemmas
Includes cic:/Flocq/Core?FIX cic:/Coq/Init?Datatypes
Includes cic:/Flocq/Core?FIX cic:/Coq/Classes?RelationClasses
Includes cic:/Flocq/Core?FIX cic:/Coq/Program?Basics
Includes cic:/Flocq/Core?FIX cic:/Coq/Classes?Morphisms
Includes cic:/Flocq/Core?FIX cic:/Coq/ZArith?BinInt/Z
Includes cic:/Flocq/Core?FIX cic:/Coq/Init?Logic
Includes cic:/Flocq/Core?FIX cic:/Coq/Reals?Rdefinitions
Includes cic:/Flocq/Core?FIX cic:/Coq/Numbers?BinNums
Includes cic:/Flocq/Core?FIX cic:/Flocq/Core?Defs
Includes cic:/Flocq/Core?FIX cic:/Flocq/Core?Zaux
Includes cic:/Flocq/Core?FIX cic:/Flocq/Core?Round_NE
Includes cic:/Flocq/Core?FIX cic:/Flocq/Core?Ulp
Includes cic:/Flocq/Core?FIX cic:/Flocq/Core?Generic_fmt
Includes cic:/Flocq/Core?FIX cic:/Flocq/Core?Round_pred
Includes cic:/Flocq/Core?FIX http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Flocq/Core?FIX cic:/Flocq/Core?Defs
Declares cic:/Flocq/Core?FIX cic:/Flocq/Core?FIX?RND_FIX
deriveddeclaration cic:/Flocq/Core?FIX?RND_FIX
Declares cic:/Flocq/Core?FIX cic:/Flocq/Core?FIX?FIX_exp
......
dataconstructor cic:/Flocq/Core?FLT?FLT_exp
dataconstructor cic:/Flocq/Core?FLT?FLT_exp_valid
dataconstructor cic:/Flocq/Core?FLT?generic_format_FLT
dataconstructor cic:/Flocq/Core?FLT?FLT_format_generic
dataconstructor cic:/Flocq/Core?FLT?FLT_format_bpow
dataconstructor cic:/Flocq/Core?FLT?FLT_format_satisfies_any
dataconstructor cic:/Flocq/Core?FLT?cexp_FLT_FLX
dataconstructor cic:/Flocq/Core?FLT?generic_format_FLT_FLX
dataconstructor cic:/Flocq/Core?FLT?generic_format_FLX_FLT
dataconstructor cic:/Flocq/Core?FLT?round_FLT_FLX
dataconstructor cic:/Flocq/Core?FLT?cexp_FLT_FIX
dataconstructor cic:/Flocq/Core?FLT?generic_format_FIX_FLT
dataconstructor cic:/Flocq/Core?FLT?generic_format_FLT_FIX
dataconstructor cic:/Flocq/Core?FLT?negligible_exp_FLT
dataconstructor cic:/Flocq/Core?FLT?generic_format_FLT_1
dataconstructor cic:/Flocq/Core?FLT?ulp_FLT_small
dataconstructor cic:/Flocq/Core?FLT?ulp_FLT_le
dataconstructor cic:/Flocq/Core?FLT?ulp_FLT_gt
dataconstructor cic:/Flocq/Core?FLT?ulp_FLT_exact_shift
dataconstructor cic:/Flocq/Core?FLT?succ_FLT_exact_shift_pos
dataconstructor cic:/Flocq/Core?FLT?succ_FLT_exact_shift
dataconstructor cic:/Flocq/Core?FLT?FLT_exp_monotone
dataconstructor cic:/Flocq/Core?FLT?exists_NE_FLT
theory cic:/Flocq/Core?FLT
HasMeta cic:/Flocq/Core?FLT http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Flocq/Core?FLT cic:/Coq/micromega?RMicromega
Includes cic:/Flocq/Core?FLT cic:/Coq/QArith?QArith_base
Includes cic:/Flocq/Core?FLT cic:/Coq/micromega?QMicromega
Includes cic:/Flocq/Core?FLT cic:/Coq/ZArith?BinIntDef/Z
Includes cic:/Flocq/Core?FLT cic:/Coq/Reals?Raxioms
Includes cic:/Flocq/Core?FLT cic:/Coq/ZArith?Zbool
Includes cic:/Flocq/Core?FLT cic:/Coq/Reals?Rfunctions
Includes cic:/Flocq/Core?FLT cic:/Coq/micromega?Tauto
Includes cic:/Flocq/Core?FLT cic:/Coq/micromega?VarMap
Includes cic:/Flocq/Core?FLT cic:/Coq/micromega?EnvRing
Includes cic:/Flocq/Core?FLT cic:/Coq/micromega?RingMicromega
Includes cic:/Flocq/Core?FLT cic:/Coq/micromega?ZMicromega
Includes cic:/Flocq/Core?FLT cic:/Coq/Classes?RelationClasses
Includes cic:/Flocq/Core?FLT cic:/Coq/Program?Basics
Includes cic:/Flocq/Core?FLT cic:/Coq/Classes?Morphisms
Includes cic:/Flocq/Core?FLT cic:/Coq/ZArith?Zmax
Includes cic:/Flocq/Core?FLT cic:/Coq/Reals?Rbasic_fun
Includes cic:/Flocq/Core?FLT cic:/Coq/Reals?RIneq
Includes cic:/Flocq/Core?FLT cic:/Coq/setoid_ring?Ring_tac
Includes cic:/Flocq/Core?FLT cic:/Coq/setoid_ring?ZArithRing
Includes cic:/Flocq/Core?FLT cic:/Coq/setoid_ring?Ring_polynom
Includes cic:/Flocq/Core?FLT cic:/Coq/ZArith?BinInt
Includes cic:/Flocq/Core?FLT cic:/Coq/ZArith?Zorder
Includes cic:/Flocq/Core?FLT cic:/Coq/ZArith?auxiliary
Includes cic:/Flocq/Core?FLT cic:/Coq/Init?Datatypes
Includes cic:/Flocq/Core?FLT cic:/Coq/omega?OmegaLemmas
Includes cic:/Flocq/Core?FLT cic:/Coq/Logic?Decidable
Includes cic:/Flocq/Core?FLT cic:/Coq/ZArith?BinInt/Z
Includes cic:/Flocq/Core?FLT cic:/Coq/Init?Logic
Includes cic:/Flocq/Core?FLT cic:/Coq/Reals?Rdefinitions
Includes cic:/Flocq/Core?FLT cic:/Coq/Numbers?BinNums
Includes cic:/Flocq/Core?FLT cic:/Coq/micromega?Psatz
Includes cic:/Flocq/Core?FLT cic:/Flocq/Core?FIX
Includes cic:/Flocq/Core?FLT cic:/Flocq/Core?Defs
Includes cic:/Flocq/Core?FLT cic:/Flocq/Core?Zaux
Includes cic:/Flocq/Core?FLT cic:/Flocq/Core?Round_NE
Includes cic:/Flocq/Core?FLT cic:/Flocq/Core?Ulp
Includes cic:/Flocq/Core?FLT cic:/Flocq/Core?FLX
Includes cic:/Flocq/Core?FLT cic:/Flocq/Core?Float_prop
Includes cic:/Flocq/Core?FLT cic:/Flocq/Core?Generic_fmt
Includes cic:/Flocq/Core?FLT cic:/Flocq/Core?Round_pred
Includes cic:/Flocq/Core?FLT http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Flocq/Core?FLT cic:/Flocq/Core?Defs
Includes cic:/Flocq/Core?FLT cic:/Flocq/Core?FIX
Includes cic:/Flocq/Core?FLT cic:/Coq/micromega?Psatz
Declares cic:/Flocq/Core?FLT cic:/Flocq/Core?FLT?RND_FLT
deriveddeclaration cic:/Flocq/Core?FLT?RND_FLT
Declares cic:/Flocq/Core?FLT cic:/Flocq/Core?FLT?FLT_exp
constant cic:/Flocq/Core?FLT?FLT_exp
Declares cic:/Flocq/Core?FLT cic:/Flocq/Core?FLT?FLT_exp_valid
constant cic:/Flocq/Core?FLT?FLT_exp_valid
Declares cic:/Flocq/Core?FLT cic:/Flocq/Core?FLT?generic_format_FLT
constant cic:/Flocq/Core?FLT?generic_format_FLT
Declares cic:/Flocq/Core?FLT cic:/Flocq/Core?FLT?FLT_format_generic
constant cic:/Flocq/Core?FLT?FLT_format_generic
Declares cic:/Flocq/Core?FLT cic:/Flocq/Core?FLT?FLT_format_bpow
constant cic:/Flocq/Core?FLT?FLT_format_bpow
Declares cic:/Flocq/Core?FLT cic:/Flocq/Core?FLT?FLT_format_satisfies_any
constant cic:/Flocq/Core?FLT?FLT_format_satisfies_any
Declares cic:/Flocq/Core?FLT cic:/Flocq/Core?FLT?cexp_FLT_FLX
constant cic:/Flocq/Core?FLT?cexp_FLT_FLX
Declares cic:/Flocq/Core?FLT cic:/Flocq/Core?FLT?generic_format_FLT_FLX
constant cic:/Flocq/Core?FLT?generic_format_FLT_FLX
Declares cic:/Flocq/Core?FLT cic:/Flocq/Core?FLT?generic_format_FLX_FLT
constant cic:/Flocq/Core?FLT?generic_format_FLX_FLT
Declares cic:/Flocq/Core?FLT cic:/Flocq/Core?FLT?round_FLT_FLX
constant cic:/Flocq/Core?FLT?round_FLT_FLX
Declares cic:/Flocq/Core?FLT cic:/Flocq/Core?FLT?cexp_FLT_FIX
constant cic:/Flocq/Core?FLT?cexp_FLT_FIX
Declares cic:/Flocq/Core?FLT cic:/Flocq/Core?FLT?generic_format_FIX_FLT
constant cic:/Flocq/Core?FLT?generic_format_FIX_FLT
Declares cic:/Flocq/Core?FLT cic:/Flocq/Core?FLT?generic_format_FLT_FIX
constant cic:/Flocq/Core?FLT?generic_format_FLT_FIX
Declares cic:/Flocq/Core?FLT cic:/Flocq/Core?FLT?negligible_exp_FLT
constant cic:/Flocq/Core?FLT?negligible_exp_FLT
Declares cic:/Flocq/Core?FLT cic:/Flocq/Core?FLT?generic_format_FLT_1
constant cic:/Flocq/Core?FLT?generic_format_FLT_1
Declares cic:/Flocq/Core?FLT cic:/Flocq/Core?FLT?ulp_FLT_small
constant cic:/Flocq/Core?FLT?ulp_FLT_small
Declares cic:/Flocq/Core?FLT cic:/Flocq/Core?FLT?ulp_FLT_le
constant cic:/Flocq/Core?FLT?ulp_FLT_le
Declares cic:/Flocq/Core?FLT cic:/Flocq/Core?FLT?ulp_FLT_gt
constant cic:/Flocq/Core?FLT?ulp_FLT_gt
Declares cic:/Flocq/Core?FLT cic:/Flocq/Core?FLT?ulp_FLT_exact_shift
constant cic:/Flocq/Core?FLT?ulp_FLT_exact_shift
Declares cic:/Flocq/Core?FLT cic:/Flocq/Core?FLT?succ_FLT_exact_shift_pos
constant cic:/Flocq/Core?FLT?succ_FLT_exact_shift_pos
Declares cic:/Flocq/Core?FLT cic:/Flocq/Core?FLT?succ_FLT_exact_shift
constant cic:/Flocq/Core?FLT?succ_FLT_exact_shift
Declares cic:/Flocq/Core?FLT cic:/Flocq/Core?FLT?FLT_exp_monotone
constant cic:/Flocq/Core?FLT?FLT_exp_monotone
Declares cic:/Flocq/Core?FLT cic:/Flocq/Core?FLT?exists_NE_FLT
constant cic:/Flocq/Core?FLT?exists_NE_FLT
dataconstructor cic:/Flocq/Core?FLX?Prec_gt_0
dataconstructor cic:/Flocq/Core?FLX?prec_gt_0
dataconstructor cic:/Flocq/Core?FLX?FLX_exp
dataconstructor cic:/Flocq/Core?FLX?FLX_exp_valid
dataconstructor cic:/Flocq/Core?FLX?FIX_format_FLX
dataconstructor cic:/Flocq/Core?FLX?FLX_format_generic
dataconstructor cic:/Flocq/Core?FLX?generic_format_FLX
dataconstructor cic:/Flocq/Core?FLX?FLX_format_satisfies_any
dataconstructor cic:/Flocq/Core?FLX?FLX_format_FIX
dataconstructor cic:/Flocq/Core?FLX?generic_format_FLXN
dataconstructor cic:/Flocq/Core?FLX?FLXN_format_generic
dataconstructor cic:/Flocq/Core?FLX?FLXN_format_satisfies_any
dataconstructor cic:/Flocq/Core?FLX?negligible_exp_FLX
dataconstructor cic:/Flocq/Core?FLX?generic_format_FLX_1
dataconstructor cic:/Flocq/Core?FLX?ulp_FLX_0
dataconstructor cic:/Flocq/Core?FLX?ulp_FLX_1
dataconstructor cic:/Flocq/Core?FLX?succ_FLX_1
dataconstructor cic:/Flocq/Core?FLX?eq_0_round_0_FLX
dataconstructor cic:/Flocq/Core?FLX?gt_0_round_gt_0_FLX
dataconstructor cic:/Flocq/Core?FLX?ulp_FLX_le
dataconstructor cic:/Flocq/Core?FLX?ulp_FLX_ge
dataconstructor cic:/Flocq/Core?FLX?ulp_FLX_exact_shift
dataconstructor cic:/Flocq/Core?FLX?succ_FLX_exact_shift
dataconstructor cic:/Flocq/Core?FLX?FLX_exp_monotone
dataconstructor cic:/Flocq/Core?FLX?exists_NE_FLX
theory cic:/Flocq/Core?FLX
HasMeta cic:/Flocq/Core?FLX http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Flocq/Core?FLX cic:/Coq/micromega?RMicromega
Includes cic:/Flocq/Core?FLX cic:/Coq/micromega?Tauto
Includes cic:/Flocq/Core?FLX cic:/Coq/micromega?VarMap
Includes cic:/Flocq/Core?FLX cic:/Coq/micromega?EnvRing
Includes cic:/Flocq/Core?FLX cic:/Coq/QArith?QArith_base
Includes cic:/Flocq/Core?FLX cic:/Coq/micromega?RingMicromega
Includes cic:/Flocq/Core?FLX cic:/Coq/micromega?QMicromega
Includes cic:/Flocq/Core?FLX cic:/Coq/ZArith?BinIntDef/Z
Includes cic:/Flocq/Core?FLX cic:/Coq/Reals?Raxioms
Includes cic:/Flocq/Core?FLX cic:/Coq/ZArith?Zbool
Includes cic:/Flocq/Core?FLX cic:/Coq/Classes?Morphisms_Prop
Includes cic:/Flocq/Core?FLX cic:/Coq/setoid_ring?Ring_tac
Includes cic:/Flocq/Core?FLX cic:/Coq/setoid_ring?ZArithRing
Includes cic:/Flocq/Core?FLX cic:/Coq/setoid_ring?Ring_polynom
Includes cic:/Flocq/Core?FLX cic:/Coq/Reals?RIneq
Includes cic:/Flocq/Core?FLX cic:/Coq/Classes?RelationClasses
Includes cic:/Flocq/Core?FLX cic:/Coq/Program?Basics
Includes cic:/Flocq/Core?FLX cic:/Coq/Classes?Morphisms
Includes cic:/Flocq/Core?FLX cic:/Coq/Reals?Rbasic_fun
Includes cic:/Flocq/Core?FLX cic:/Coq/ZArith?Zorder
Includes cic:/Flocq/Core?FLX cic:/Coq/ZArith?auxiliary
Includes cic:/Flocq/Core?FLX cic:/Coq/Init?Datatypes
Includes cic:/Flocq/Core?FLX cic:/Coq/omega?OmegaLemmas
Includes cic:/Flocq/Core?FLX cic:/Coq/Logic?Decidable
Includes cic:/Flocq/Core?FLX cic:/Coq/Init?Logic
Includes cic:/Flocq/Core?FLX cic:/Coq/Reals?Rdefinitions
Includes cic:/Flocq/Core?FLX cic:/Coq/ZArith?BinInt/Z
Includes cic:/Flocq/Core?FLX cic:/Coq/Numbers?BinNums
Includes cic:/Flocq/Core?FLX cic:/Coq/micromega?Psatz
Includes cic:/Flocq/Core?FLX cic:/Flocq/Core?FIX
Includes cic:/Flocq/Core?FLX cic:/Flocq/Core?Defs
Includes cic:/Flocq/Core?FLX cic:/Flocq/Core?Zaux
Includes cic:/Flocq/Core?FLX cic:/Flocq/Core?Round_NE
Includes cic:/Flocq/Core?FLX cic:/Flocq/Core?Ulp
Includes cic:/Flocq/Core?FLX cic:/Flocq/Core?Float_prop
Includes cic:/Flocq/Core?FLX cic:/Flocq/Core?Generic_fmt
Includes cic:/Flocq/Core?FLX cic:/Flocq/Core?Round_pred
Includes cic:/Flocq/Core?FLX http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Flocq/Core?FLX cic:/Flocq/Core?Defs
Includes cic:/Flocq/Core?FLX cic:/Flocq/Core?FIX
Includes cic:/Flocq/Core?FLX cic:/Coq/micromega?Psatz
Declares cic:/Flocq/Core?FLX cic:/Flocq/Core?FLX?RND_FLX
deriveddeclaration cic:/Flocq/Core?FLX?RND_FLX
Declares cic:/Flocq/Core?FLX cic:/Flocq/Core?FLX?Prec_gt_0
constant cic:/Flocq/Core?FLX?Prec_gt_0
Declares cic:/Flocq/Core?FLX cic:/Flocq/Core?FLX?prec_gt_0
constant cic:/Flocq/Core?FLX?prec_gt_0
Declares cic:/Flocq/Core?FLX cic:/Flocq/Core?FLX?FLX_exp
constant cic:/Flocq/Core?FLX?FLX_exp
Declares cic:/Flocq/Core?FLX cic:/Flocq/Core?FLX?FLX_exp_valid
constant cic:/Flocq/Core?FLX?FLX_exp_valid
Declares cic:/Flocq/Core?FLX cic:/Flocq/Core?FLX?FIX_format_FLX
constant cic:/Flocq/Core?FLX?FIX_format_FLX
Declares cic:/Flocq/Core?FLX cic:/Flocq/Core?FLX?FLX_format_generic
constant cic:/Flocq/Core?FLX?FLX_format_generic
Declares cic:/Flocq/Core?FLX cic:/Flocq/Core?FLX?generic_format_FLX
constant cic:/Flocq/Core?FLX?generic_format_FLX
Declares cic:/Flocq/Core?FLX cic:/Flocq/Core?FLX?FLX_format_satisfies_any
constant cic:/Flocq/Core?FLX?FLX_format_satisfies_any
Declares cic:/Flocq/Core?FLX cic:/Flocq/Core?FLX?FLX_format_FIX
constant cic:/Flocq/Core?FLX?FLX_format_FIX
Declares cic:/Flocq/Core?FLX cic:/Flocq/Core?FLX?generic_format_FLXN
constant cic:/Flocq/Core?FLX?generic_format_FLXN
Declares cic:/Flocq/Core?FLX cic:/Flocq/Core?FLX?FLXN_format_generic
constant cic:/Flocq/Core?FLX?FLXN_format_generic
Declares cic:/Flocq/Core?FLX cic:/Flocq/Core?FLX?FLXN_format_satisfies_any
constant cic:/Flocq/Core?FLX?FLXN_format_satisfies_any
Declares cic:/Flocq/Core?FLX cic:/Flocq/Core?FLX?negligible_exp_FLX
constant cic:/Flocq/Core?FLX?negligible_exp_FLX
Declares cic:/Flocq/Core?FLX cic:/Flocq/Core?FLX?generic_format_FLX_1
constant cic:/Flocq/Core?FLX?generic_format_FLX_1
Declares cic:/Flocq/Core?FLX cic:/Flocq/Core?FLX?ulp_FLX_0
constant cic:/Flocq/Core?FLX?ulp_FLX_0
Declares cic:/Flocq/Core?FLX cic:/Flocq/Core?FLX?ulp_FLX_1
constant cic:/Flocq/Core?FLX?ulp_FLX_1
Declares cic:/Flocq/Core?FLX cic:/Flocq/Core?FLX?succ_FLX_1
constant cic:/Flocq/Core?FLX?succ_FLX_1
Declares cic:/Flocq/Core?FLX cic:/Flocq/Core?FLX?eq_0_round_0_FLX
constant cic:/Flocq/Core?FLX?eq_0_round_0_FLX
Declares cic:/Flocq/Core?FLX cic:/Flocq/Core?FLX?gt_0_round_gt_0_FLX
constant cic:/Flocq/Core?FLX?gt_0_round_gt_0_FLX
Declares cic:/Flocq/Core?FLX cic:/Flocq/Core?FLX?ulp_FLX_le
constant cic:/Flocq/Core?FLX?ulp_FLX_le
Declares cic:/Flocq/Core?FLX cic:/Flocq/Core?FLX?ulp_FLX_ge
constant cic:/Flocq/Core?FLX?ulp_FLX_ge
Declares cic:/Flocq/Core?FLX cic:/Flocq/Core?FLX?ulp_FLX_exact_shift
constant cic:/Flocq/Core?FLX?ulp_FLX_exact_shift
Declares cic:/Flocq/Core?FLX cic:/Flocq/Core?FLX?succ_FLX_exact_shift
constant cic:/Flocq/Core?FLX?succ_FLX_exact_shift
Declares cic:/Flocq/Core?FLX cic:/Flocq/Core?FLX?FLX_exp_monotone
constant cic:/Flocq/Core?FLX?FLX_exp_monotone
Declares cic:/Flocq/Core?FLX cic:/Flocq/Core?FLX?exists_NE_FLX
constant cic:/Flocq/Core?FLX?exists_NE_FLX
......@@ -30,7 +30,12 @@ Includes cic:/Flocq/Core?FTZ cic:/Coq/ZArith?BinInt/Z
Includes cic:/Flocq/Core?FTZ cic:/Coq/Init?Logic
Includes cic:/Flocq/Core?FTZ cic:/Coq/Reals?Rdefinitions
Includes cic:/Flocq/Core?FTZ cic:/Coq/Numbers?BinNums
Includes cic:/Flocq/Core?FTZ cic:/Flocq/Core?Zaux
Includes cic:/Flocq/Core?FTZ cic:/Flocq/Core?FLX
Includes cic:/Flocq/Core?FTZ cic:/Flocq/Core?Ulp
Includes cic:/Flocq/Core?FTZ cic:/Flocq/Core?Float_prop
Includes cic:/Flocq/Core?FTZ cic:/Flocq/Core?Generic_fmt
Includes cic:/Flocq/Core?FTZ cic:/Flocq/Core?Round_pred
Includes cic:/Flocq/Core?FTZ cic:/Flocq/Core?Defs
Includes cic:/Flocq/Core?FTZ http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/Flocq/Core?FTZ cic:/Flocq/Core?FTZ?RND_FTZ
......
dataconstructor cic:/Flocq/Core?Float_prop?Rcompare_F2R
dataconstructor cic:/Flocq/Core?Float_prop?le_F2R
dataconstructor cic:/Flocq/Core?Float_prop?F2R_le
dataconstructor cic:/Flocq/Core?Float_prop?lt_F2R
dataconstructor cic:/Flocq/Core?Float_prop?F2R_lt
dataconstructor cic:/Flocq/Core?Float_prop?F2R_eq
dataconstructor cic:/Flocq/Core?Float_prop?eq_F2R
dataconstructor cic:/Flocq/Core?Float_prop?F2R_Zabs
dataconstructor cic:/Flocq/Core?Float_prop?F2R_Zopp
dataconstructor cic:/Flocq/Core?Float_prop?F2R_cond_Zopp
dataconstructor cic:/Flocq/Core?Float_prop?F2R_0
dataconstructor cic:/Flocq/Core?Float_prop?eq_0_F2R
dataconstructor cic:/Flocq/Core?Float_prop?ge_0_F2R
dataconstructor cic:/Flocq/Core?Float_prop?le_0_F2R
dataconstructor cic:/Flocq/Core?Float_prop?gt_0_F2R
dataconstructor cic:/Flocq/Core?Float_prop?lt_0_F2R
dataconstructor cic:/Flocq/Core?Float_prop?F2R_ge_0
dataconstructor cic:/Flocq/Core?Float_prop?F2R_le_0
dataconstructor cic:/Flocq/Core?Float_prop?F2R_gt_0
dataconstructor cic:/Flocq/Core?Float_prop?F2R_lt_0
dataconstructor cic:/Flocq/Core?Float_prop?F2R_neq_0
dataconstructor cic:/Flocq/Core?Float_prop?Fnum_ge_0
dataconstructor cic:/Flocq/Core?Float_prop?Fnum_le_0
dataconstructor cic:/Flocq/Core?Float_prop?F2R_bpow
dataconstructor cic:/Flocq/Core?Float_prop?bpow_le_F2R
dataconstructor cic:/Flocq/Core?Float_prop?F2R_p1_le_bpow
dataconstructor cic:/Flocq/Core?Float_prop?bpow_le_F2R_m1
dataconstructor cic:/Flocq/Core?Float_prop?F2R_lt_bpow
dataconstructor cic:/Flocq/Core?Float_prop?F2R_change_exp
dataconstructor cic:/Flocq/Core?Float_prop?F2R_prec_normalize
dataconstructor cic:/Flocq/Core?Float_prop?mag_F2R_bounds
dataconstructor cic:/Flocq/Core?Float_prop?mag_F2R
dataconstructor cic:/Flocq/Core?Float_prop?Zdigits_mag
dataconstructor cic:/Flocq/Core?Float_prop?mag_F2R_Zdigits
dataconstructor cic:/Flocq/Core?Float_prop?mag_F2R_bounds_Zdigits
dataconstructor cic:/Flocq/Core?Float_prop?float_distribution_pos
theory cic:/Flocq/Core?Float_prop
HasMeta cic:/Flocq/Core?Float_prop http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Flocq/Core?Float_prop cic:/Coq/ZArith?auxiliary
Includes cic:/Flocq/Core?Float_prop cic:/Coq/omega?OmegaLemmas
Includes cic:/Flocq/Core?Float_prop cic:/Coq/Logic?Decidable
Includes cic:/Flocq/Core?Float_prop cic:/Coq/ZArith?BinInt
Includes cic:/Flocq/Core?Float_prop cic:/Coq/setoid_ring?Ring_tac
Includes cic:/Flocq/Core?Float_prop cic:/Coq/setoid_ring?ZArithRing
Includes cic:/Flocq/Core?Float_prop cic:/Coq/setoid_ring?Ring_polynom
Includes cic:/Flocq/Core?Float_prop cic:/Coq/Classes?RelationClasses
Includes cic:/Flocq/Core?Float_prop cic:/Coq/Program?Basics
Includes cic:/Flocq/Core?Float_prop cic:/Coq/Classes?Morphisms
Includes cic:/Flocq/Core?Float_prop cic:/Coq/ZArith?Zorder
Includes cic:/Flocq/Core?Float_prop cic:/Coq/Reals?Raxioms
Includes cic:/Flocq/Core?Float_prop cic:/Coq/Reals?Rbasic_fun
Includes cic:/Flocq/Core?Float_prop cic:/Coq/Reals?RIneq
Includes cic:/Flocq/Core?Float_prop cic:/Coq/ZArith?BinInt/Z
Includes cic:/Flocq/Core?Float_prop cic:/Coq/Reals?Rdefinitions
Includes cic:/Flocq/Core?Float_prop cic:/Coq/Init?Datatypes
Includes cic:/Flocq/Core?Float_prop cic:/Coq/Init?Logic
Includes cic:/Flocq/Core?Float_prop cic:/Coq/Numbers?BinNums
Includes cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Digits
Includes cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Defs
Includes cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Zaux
Includes cic:/Flocq/Core?Float_prop http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Defs
Includes cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Digits
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?Float_prop
deriveddeclaration cic:/Flocq/Core?Float_prop?Float_prop
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?Rcompare_F2R
constant cic:/Flocq/Core?Float_prop?Rcompare_F2R
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?le_F2R
constant cic:/Flocq/Core?Float_prop?le_F2R
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?F2R_le
constant cic:/Flocq/Core?Float_prop?F2R_le
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?lt_F2R
constant cic:/Flocq/Core?Float_prop?lt_F2R
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?F2R_lt
constant cic:/Flocq/Core?Float_prop?F2R_lt
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?F2R_eq
constant cic:/Flocq/Core?Float_prop?F2R_eq
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?eq_F2R
constant cic:/Flocq/Core?Float_prop?eq_F2R
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?F2R_Zabs
constant cic:/Flocq/Core?Float_prop?F2R_Zabs
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?F2R_Zopp
constant cic:/Flocq/Core?Float_prop?F2R_Zopp
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?F2R_cond_Zopp
constant cic:/Flocq/Core?Float_prop?F2R_cond_Zopp
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?F2R_0
constant cic:/Flocq/Core?Float_prop?F2R_0
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?eq_0_F2R
constant cic:/Flocq/Core?Float_prop?eq_0_F2R
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?ge_0_F2R
constant cic:/Flocq/Core?Float_prop?ge_0_F2R
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?le_0_F2R
constant cic:/Flocq/Core?Float_prop?le_0_F2R
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?gt_0_F2R
constant cic:/Flocq/Core?Float_prop?gt_0_F2R
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?lt_0_F2R
constant cic:/Flocq/Core?Float_prop?lt_0_F2R
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?F2R_ge_0
constant cic:/Flocq/Core?Float_prop?F2R_ge_0
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?F2R_le_0
constant cic:/Flocq/Core?Float_prop?F2R_le_0
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?F2R_gt_0
constant cic:/Flocq/Core?Float_prop?F2R_gt_0
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?F2R_lt_0
constant cic:/Flocq/Core?Float_prop?F2R_lt_0
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?F2R_neq_0
constant cic:/Flocq/Core?Float_prop?F2R_neq_0
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?Fnum_ge_0
constant cic:/Flocq/Core?Float_prop?Fnum_ge_0
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?Fnum_le_0
constant cic:/Flocq/Core?Float_prop?Fnum_le_0
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?F2R_bpow
constant cic:/Flocq/Core?Float_prop?F2R_bpow
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?bpow_le_F2R
constant cic:/Flocq/Core?Float_prop?bpow_le_F2R
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?F2R_p1_le_bpow
constant cic:/Flocq/Core?Float_prop?F2R_p1_le_bpow
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?bpow_le_F2R_m1
constant cic:/Flocq/Core?Float_prop?bpow_le_F2R_m1
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?F2R_lt_bpow
constant cic:/Flocq/Core?Float_prop?F2R_lt_bpow
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?F2R_change_exp
constant cic:/Flocq/Core?Float_prop?F2R_change_exp
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?F2R_prec_normalize
constant cic:/Flocq/Core?Float_prop?F2R_prec_normalize
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?mag_F2R_bounds
constant cic:/Flocq/Core?Float_prop?mag_F2R_bounds
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?mag_F2R
constant cic:/Flocq/Core?Float_prop?mag_F2R
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?Zdigits_mag
constant cic:/Flocq/Core?Float_prop?Zdigits_mag
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?mag_F2R_Zdigits
constant cic:/Flocq/Core?Float_prop?mag_F2R_Zdigits
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?mag_F2R_bounds_Zdigits
constant cic:/Flocq/Core?Float_prop?mag_F2R_bounds_Zdigits
Declares cic:/Flocq/Core?Float_prop cic:/Flocq/Core?Float_prop?float_distribution_pos
constant cic:/Flocq/Core?Float_prop?float_distribution_pos
dataconstructor cic:/Flocq/Core?Round_NE?NE_prop
dataconstructor cic:/Flocq/Core?Round_NE?Rnd_NE_pt
dataconstructor cic:/Flocq/Core?Round_NE?DN_UP_parity_pos_prop
dataconstructor cic:/Flocq/Core?Round_NE?DN_UP_parity_prop
dataconstructor cic:/Flocq/Core?Round_NE?DN_UP_parity_aux
dataconstructor cic:/Flocq/Core?Round_NE?Exists_NE
dataconstructor cic:/Flocq/Core?Round_NE?exists_NE
dataconstructor cic:/Flocq/Core?Round_NE?DN_UP_parity_generic_pos
dataconstructor cic:/Flocq/Core?Round_NE?DN_UP_parity_generic
dataconstructor cic:/Flocq/Core?Round_NE?Rnd_NE_pt_total
dataconstructor cic:/Flocq/Core?Round_NE?Rnd_NE_pt_monotone
dataconstructor cic:/Flocq/Core?Round_NE?Rnd_NE_pt_round
dataconstructor cic:/Flocq/Core?Round_NE?round_NE_pt_pos
dataconstructor cic:/Flocq/Core?Round_NE?round_NE_opp
dataconstructor cic:/Flocq/Core?Round_NE?round_NE_abs
dataconstructor cic:/Flocq/Core?Round_NE?round_NE_pt
theory cic:/Flocq/Core?Round_NE
HasMeta cic:/Flocq/Core?Round_NE http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Flocq/Core?Round_NE cic:/Coq/ZArith?BinInt
Includes cic:/Flocq/Core?Round_NE cic:/Coq/ZArith?ZArith_dec
Includes cic:/Flocq/Core?Round_NE cic:/Coq/Classes?RelationClasses
Includes cic:/Flocq/Core?Round_NE cic:/Coq/Classes?Morphisms_Prop
Includes cic:/Flocq/Core?Round_NE cic:/Coq/Program?Basics
Includes cic:/Flocq/Core?Round_NE cic:/Coq/Classes?Morphisms
Includes cic:/Flocq/Core?Round_NE cic:/Coq/ZArith?auxiliary
Includes cic:/Flocq/Core?Round_NE cic:/Coq/omega?OmegaLemmas
Includes cic:/Flocq/Core?Round_NE cic:/Coq/Logic?Decidable
Includes cic:/Flocq/Core?Round_NE cic:/Coq/setoid_ring?Ring_tac
Includes cic:/Flocq/Core?Round_NE cic:/Coq/setoid_ring?ZArithRing
Includes cic:/Flocq/Core?Round_NE cic:/Coq/setoid_ring?Ring_polynom
Includes cic:/Flocq/Core?Round_NE cic:/Coq/ZArith?Zorder
Includes cic:/Flocq/Core?Round_NE cic:/Coq/Reals?Rbasic_fun
Includes cic:/Flocq/Core?Round_NE cic:/Coq/Bool?Bool
Includes cic:/Flocq/Core?Round_NE cic:/Coq/Reals?RIneq
Includes cic:/Flocq/Core?Round_NE cic:/Coq/Init?Specif
Includes cic:/Flocq/Core?Round_NE cic:/Coq/Reals?Raxioms
Includes cic:/Flocq/Core?Round_NE cic:/Coq/ZArith?BinInt/Z
Includes cic:/Flocq/Core?Round_NE cic:/Coq/Init?Datatypes
Includes cic:/Flocq/Core?Round_NE cic:/Coq/Init?Logic
Includes cic:/Flocq/Core?Round_NE cic:/Coq/Reals?Rdefinitions
Includes cic:/Flocq/Core?Round_NE cic:/Coq/Numbers?BinNums
Includes cic:/Flocq/Core?Round_NE cic:/Flocq/Core?Float_prop
Includes cic:/Flocq/Core?Round_NE cic:/Flocq/Core?Generic_fmt
Includes cic:/Flocq/Core?Round_NE cic:/Flocq/Core?Defs
Includes cic:/Flocq/Core?Round_NE cic:/Flocq/Core?Zaux
Includes cic:/Flocq/Core?Round_NE cic:/Flocq/Core?Ulp
Includes cic:/Flocq/Core?Round_NE cic:/Flocq/Core?Round_pred
Includes cic:/Flocq/Core?Round_NE cic:/Flocq/Core?Raux
Includes cic:/Flocq/Core?Round_NE http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/Flocq/Core?Round_NE cic:/Flocq/Core?Defs
Includes cic:/Flocq/Core?Round_NE cic:/Flocq/Core?Generic_fmt
Includes cic:/Flocq/Core?Round_NE cic:/Flocq/Core?Float_prop
Declares cic:/Flocq/Core?Round_NE cic:/Flocq/Core?Round_NE?Fcore_rnd_NE
deriveddeclaration cic:/Flocq/Core?Round_NE?Fcore_rnd_NE
Declares cic:/Flocq/Core?Round_NE cic:/Flocq/Core?Round_NE?NE_prop
constant cic:/Flocq/Core?Round_NE?NE_prop
Declares cic:/Flocq/Core?Round_NE cic:/Flocq/Core?Round_NE?Rnd_NE_pt
constant cic:/Flocq/Core?Round_NE?Rnd_NE_pt
Declares cic:/Flocq/Core?Round_NE cic:/Flocq/Core?Round_NE?DN_UP_parity_pos_prop
constant cic:/Flocq/Core?Round_NE?DN_UP_parity_pos_prop
Declares cic:/Flocq/Core?Round_NE cic:/Flocq/Core?Round_NE?DN_UP_parity_prop
constant cic:/Flocq/Core?Round_NE?DN_UP_parity_prop
Declares cic:/Flocq/Core?Round_NE cic:/Flocq/Core?Round_NE?DN_UP_parity_aux
constant cic:/Flocq/Core?Round_NE?DN_UP_parity_aux
Declares cic:/Flocq/Core?Round_NE cic:/Flocq/Core?Round_NE?Exists_NE
constant cic:/Flocq/Core?Round_NE?Exists_NE
Declares cic:/Flocq/Core?Round_NE cic:/Flocq/Core?Round_NE?exists_NE
constant cic:/Flocq/Core?Round_NE?exists_NE
Declares cic:/Flocq/Core?Round_NE cic:/Flocq/Core?Round_NE?DN_UP_parity_generic_pos
constant cic:/Flocq/Core?Round_NE?DN_UP_parity_generic_pos
Declares cic:/Flocq/Core?Round_NE cic:/Flocq/Core?Round_NE?DN_UP_parity_generic
constant cic:/Flocq/Core?Round_NE?DN_UP_parity_generic
Declares cic:/Flocq/Core?Round_NE cic:/Flocq/Core?Round_NE?Rnd_NE_pt_total
constant cic:/Flocq/Core?Round_NE?Rnd_NE_pt_total
Declares cic:/Flocq/Core?Round_NE cic:/Flocq/Core?Round_NE?Rnd_NE_pt_monotone
constant cic:/Flocq/Core?Round_NE?Rnd_NE_pt_monotone
Declares cic:/Flocq/Core?Round_NE cic:/Flocq/Core?Round_NE?Rnd_NE_pt_round
constant cic:/Flocq/Core?Round_NE?Rnd_NE_pt_round
Declares cic:/Flocq/Core?Round_NE cic:/Flocq/Core?Round_NE?round_NE_pt_pos
constant cic:/Flocq/Core?Round_NE?round_NE_pt_pos
Declares cic:/Flocq/Core?Round_NE cic:/Flocq/Core?Round_NE?round_NE_opp
constant cic:/Flocq/Core?Round_NE?round_NE_opp
Declares cic:/Flocq/Core?Round_NE cic:/Flocq/Core?Round_NE?round_NE_abs
constant cic:/Flocq/Core?Round_NE?round_NE_abs
Declares cic:/Flocq/Core?Round_NE cic:/Flocq/Core?Round_NE?round_NE_pt
constant cic:/Flocq/Core?Round_NE?round_NE_pt
This diff is collapsed.
This diff is collapsed.
......@@ -181,6 +181,7 @@ Includes cic:/Flocq/IEEE754?Binary cic:/Flocq/Core?Zaux
Includes cic:/Flocq/IEEE754?Binary cic:/Coq/Numbers?BinNums
Includes cic:/Flocq/IEEE754?Binary cic:/Coq/Init?Datatypes
Includes cic:/Flocq/IEEE754?Binary cic:/Coq/micromega?Psatz
Includes cic:/Flocq/IEEE754?Binary cic:/Flocq/Prop?Relative
Includes cic:/Flocq/IEEE754?Binary cic:/Flocq/Calc?Sqrt
Includes cic:/Flocq/IEEE754?Binary cic:/Flocq/Calc?Div
Includes cic:/Flocq/IEEE754?Binary cic:/Flocq/Calc?Operations
......@@ -188,7 +189,6 @@ Includes cic:/Flocq/IEEE754?Binary cic:/Flocq/Calc?Bracket
Includes cic:/Flocq/IEEE754?Binary cic:/Flocq/Calc?Round
Includes cic:/Flocq/IEEE754?Binary cic:/Flocq/Core?Digits
Includes cic:/Flocq/IEEE754?Binary cic:/Flocq/Core?Core
Includes cic:/Flocq/IEEE754?Binary http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/Flocq/IEEE754?Binary cic:/Flocq/IEEE754?Binary?AnyRadix
deriveddeclaration cic:/Flocq/IEEE754?Binary?AnyRadix
Declares cic:/Flocq/IEEE754?Binary cic:/Flocq/IEEE754?Binary?FF2R
......
......@@ -91,7 +91,11 @@ Includes cic:/Flocq/Pff?Pff2Flocq cic:/Flocq/Core?FLX
Includes cic:/Flocq/Pff?Pff2Flocq cic:/Coq/ZArith?BinInt/Z
Includes cic:/Flocq/Pff?Pff2Flocq cic:/Coq/Init?Datatypes
Includes cic:/Flocq/Pff?Pff2Flocq cic:/Coq/Numbers?BinNums
Includes cic:/Flocq/Pff?Pff2Flocq cic:/Flocq/Pff?Pff2FlocqAux
Includes cic:/Flocq/Pff?Pff2Flocq cic:/Flocq/Prop?Sterbenz
Includes cic:/Flocq/Pff?Pff2Flocq cic:/Flocq/Calc?Operations
Includes cic:/Flocq/Pff?Pff2Flocq cic:/Flocq/Prop?Mult_error
Includes cic:/Flocq/Pff?Pff2Flocq cic:/Flocq/Prop?Plus_error
Includes cic:/Flocq/Pff?Pff2Flocq cic:/Flocq/Core?Core
Includes cic:/Flocq/Pff?Pff2Flocq cic:/Coq/micromega?Psatz
Includes cic:/Flocq/Pff?Pff2Flocq http://coq.inria.fr/foundation?CoqSyntax
......
......@@ -69,10 +69,12 @@ Includes cic:/Flocq/Prop?Div_sqrt_error cic:/Coq/Reals?Rdefinitions
Includes cic:/Flocq/Prop?Div_sqrt_error cic:/Coq/ZArith?BinInt/Z
Includes cic:/Flocq/Prop?Div_sqrt_error cic:/