summaryrefslogtreecommitdiff
path: root/contrib/interface/xlate.mli
blob: 2e2b95fe7df4ae73f4cda0f8a2a8c4548066b678 (plain)
1
2
3
4
5
6
7
8
open Ascent;;

val xlate_vernac : Vernacexpr.vernac_expr -> ct_COMMAND;;
val xlate_tactic : Tacexpr.raw_tactic_expr -> ct_TACTIC_COM;;
val xlate_formula : Topconstr.constr_expr -> ct_FORMULA;;
val xlate_ident : Names.identifier -> ct_ID;;
val xlate_vernac_list : Vernacexpr.vernac_expr -> ct_COMMAND_LIST;;