You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
When extracting to ocaml, native ints are extracted to Uint63.t.
However, file native-coq/theories/Array/ExtractNative.v still extracts constants using implementation native-coq/theories/Array/extrNative.ml instead of native-coq/kernel/uint63.ml.
In order to update ExtractNative.v, we need to implement a few missing bits in uint63.ml, like foldi_cont, foldi_down_cont, print_uint and probably a few others.
The text was updated successfully, but these errors were encountered:
When extracting to ocaml, native ints are extracted to Uint63.t.
However, file
native-coq/theories/Array/ExtractNative.v
still extracts constants using implementationnative-coq/theories/Array/extrNative.ml
instead ofnative-coq/kernel/uint63.ml
.In order to update
ExtractNative.v
, we need to implement a few missing bits inuint63.ml
, likefoldi_cont
,foldi_down_cont
,print_uint
and probably a few others.The text was updated successfully, but these errors were encountered: