diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/09867-primitive-floats.sh | 12 | ||||
| -rw-r--r-- | dev/top_printers.ml | 4 | ||||
| -rw-r--r-- | dev/vm_printers.ml | 1 |
3 files changed, 17 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/09867-primitive-floats.sh b/dev/ci/user-overlays/09867-primitive-floats.sh new file mode 100644 index 0000000000..a0e9085afd --- /dev/null +++ b/dev/ci/user-overlays/09867-primitive-floats.sh @@ -0,0 +1,12 @@ +if [ "$CI_PULL_REQUEST" = "9867" ] || [ "$CI_BRANCH" = "primitive-floats" ]; then + + unicoq_CI_REF=primitive-floats + unicoq_CI_GITURL=https://github.com/validsdp/unicoq + + elpi_CI_REF=primitive-floats + elpi_CI_GITURL=https://github.com/validsdp/coq-elpi + + coqhammer_CI_REF=primitive-floats + coqhammer_CI_GITURL=https://github.com/validsdp/coqhammer + +fi diff --git a/dev/top_printers.ml b/dev/top_printers.ml index aa28bce018..ccb8658eee 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -307,6 +307,8 @@ let constr_display csr = ^(array_display bl)^")" | Int i -> "Int("^(Uint63.to_string i)^")" + | Float f -> + "Float("^(Float64.to_string f)^")" and array_display v = "[|"^ @@ -439,6 +441,8 @@ let print_pure_constr csr = in print_string"{"; print_fix (); print_string"}" | Int i -> print_string ("Int("^(Uint63.to_string i)^")") + | Float f -> + print_string ("Float("^(Float64.to_string f)^")") and box_display c = open_hovbox 1; term_display c; close_box() diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index 863d930968..11565b99eb 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -84,6 +84,7 @@ and ppwhd whd = | Vconstr_const i -> print_string "C(";print_int i;print_string")" | Vconstr_block b -> ppvblock b | Vint64 i -> printf "int64(%LiL)" i + | Vfloat64 f -> printf "float64(%.17g)" f | Vatom_stk(a,s) -> open_hbox();ppatom a;close_box(); print_string"@";ppstack s |