sig
  val typ : Coq.lazy_ref
  val some : EConstr.constr -> EConstr.constr -> EConstr.constr
  val none : EConstr.constr -> EConstr.constr
  val of_option : EConstr.constr -> EConstr.constr option -> EConstr.constr
end