module Sigma:sig
..end
Environments
val add : EConstr.constr ->
EConstr.constr -> EConstr.constr -> EConstr.constr -> EConstr.constr
add ty n x map
adds the value x
of type ty
with key n
in map
val empty : EConstr.constr -> EConstr.constr
empty ty
create an empty map of type ty
val of_list : EConstr.constr ->
EConstr.constr -> (int * EConstr.constr) list -> EConstr.constr
of_list ty null l
translates an OCaml association list into a Coq one
val to_fun : EConstr.constr -> EConstr.constr -> EConstr.constr -> EConstr.constr
to_fun ty null map
converts a Coq association list into a Coq function (with default value null
)