blob: 754ccb69aab75225703b8bec5dfa5ccde7b82024 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Require Import Floats.
Goal True.
pose (f := one).
pose (f' := (-f)%float).
(* this used to segfault when the coq_env array given to the
coq_interprete C function was an unboxed OCaml Double_array
(created by Array.map in csymtable.ml just before calling
eval_tcode) *)
vm_compute in f'.
Abort.
|
