type add_ml = Mltop.add_ml = | AddNoML| AddTopML| AddRecML
val add_ml_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> add_mlval sexp_of_add_ml : add_ml -> Ppx_sexp_conv_lib.Sexp.ttype vo_path_spec = Mltop.vo_path_spec = {unix_path : string;coq_path : Names.DirPath.t;implicit : bool;has_ml : add_ml;
}val vo_path_spec_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> vo_path_specval sexp_of_vo_path_spec : vo_path_spec -> Ppx_sexp_conv_lib.Sexp.ttype coq_path_spec = Mltop.coq_path_spec = | VoPath of vo_path_spec| MlPath of string
val coq_path_spec_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> coq_path_specval sexp_of_coq_path_spec : coq_path_spec -> Ppx_sexp_conv_lib.Sexp.ttype coq_path = Mltop.coq_path = {path_spec : coq_path_spec;recursive : bool;
}val coq_path_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> coq_pathval sexp_of_coq_path : coq_path -> Ppx_sexp_conv_lib.Sexp.t