Module Theory.Sigma

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)