summaryrefslogtreecommitdiff
path: root/contrib/interface/xlate.mli
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface/xlate.mli')
-rw-r--r--contrib/interface/xlate.mli8
1 files changed, 0 insertions, 8 deletions
diff --git a/contrib/interface/xlate.mli b/contrib/interface/xlate.mli
deleted file mode 100644
index 2e2b95fe..00000000
--- a/contrib/interface/xlate.mli
+++ /dev/null
@@ -1,8 +0,0 @@
-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;;
-