Index of values

A
add [Store]
add_register_handler [Interfaces]
assign [Heap]	Change the Coq term identified by the reference passed as an argument.
assign [Refs]
B
bool_of_coqbool [Coqbool]
bool_to_coqbool [Coqbool]
C
char_of_coqbyte [Coqbyte]
char_to_coqbyte [Coqbyte]
coqbyte_t [Coqbyte]
coqi63_t [Coqi63]
coqlist_cons [Coqlist]
coqlist_fold_left [Coqlist]
coqlist_iteri [Coqlist]
coqlist_nil [Coqlist]
coqlist_t [Coqlist]
coqprod_t [Coqprod]
coqtt [Coqunit]
create [Store]
D
deref [Heap]	Return the Coq term identified by the reference passed as an argument.
deref [Refs]
destruct [Heap]	Remove the Coq term identified by the reference passed as an argument from the so-called heap.
F
find [Store]
find [Resources]
force_interface_initializers [Interfaces]
I
insert [Resources]
int_of_coqi63 [Coqi63]
int_of_coqint [Coqi63]
int_to_coqi63 [Coqi63]
int_to_coqint [Coqi63]
L
list_of_coqlist [Coqlist]
list_to_coqlist [Coqlist]
M
make_ref [Heap]	Store a Coq term inside the so-called heap, and return a reference to manipulate it.
make_ref [Refs]
N
new_primitive [Interfaces]
P
primitive_semantic [Interfaces]
prod_of_coqprod [Coqprod]
prod_to_coqprod [Coqprod]
R
register_interface [Extends]	After `register_interface modpath [(cname1, sem1); ...; (cnamen, semn)]` has been executed, primitives constructed with constructors `cname1` to `cnamen` (which lives in the module defined by `modpath`) will be supported by the `Exec` command, which will use `sem1` to `semn` to realize them.
remove [Store]
remove [Resources]
replace [Store]
replace [Resources]
S
sum_of_coqsum [Coqsum]
sum_to_coqsum [Coqsum]