aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/interface/name_to_ast.mli
blob: db2555550e4b87660c3fb2c1909aae39d2c62565 (plain)
1
2
3
4
5
val name_to_ast : Libnames.reference -> Vernacexpr.vernac_expr;;
val inductive_to_ast_list : Names.mutual_inductive -> Vernacexpr.vernac_expr list;;
val constant_to_ast_list : Names.constant -> Vernacexpr.vernac_expr list;;
val variable_to_ast_list : Names.variable -> Vernacexpr.vernac_expr list;;
val leaf_entry_to_ast_list : (Libnames.full_path * Names.kernel_name) * Libobject.obj -> Vernacexpr.vernac_expr list;;