complete Coq realizations
Currently some Coq realizations have some occurrences of Admitted
. This should be fixed. Here is the list
-
lib/coq/bv/BV_gen.v
-
lib/coq/ieee_float/Float32.v
-
lib/coq/ieee_float/Float64.v
-
lib/coq/ieee_float/GenericFloat.v
-
lib/coq/real/Trigonometry.v
-
lib/coq/set/Set.v