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