summaryrefslogtreecommitdiff
path: root/contrib/interface/name_to_ast.mli
blob: f9e83b5e1ecd7f4c6d78c1e2b9839ff65750e4af (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.section_path * Names.mutual_inductive) * Libobject.obj -> Vernacexpr.vernac_expr list;;