maximedenes/native-coq — Issue #2: Write / Restore State incompatible with native compilation
Author: maximedenes
Created: 2011-12-13 19:06:18+00:00
State: open

Definition b := true.
Write State "foo_state".
Restore State "foo_state".
cannot find file /home/mdenes/native-coq/kernel/foo_state.coq.cmxs in search path

Eval native_compute in b.
Compilation...
File "/tmp/Coq_native6784ac.ml", line 6, characters 2-14:
Error: Unbound value const_NTop_b
Anomaly: Compilation failure. Please report.