summaryrefslogtreecommitdiff
path: root/contrib/interface/translate.mli
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface/translate.mli')
-rw-r--r--contrib/interface/translate.mli12
1 files changed, 0 insertions, 12 deletions
diff --git a/contrib/interface/translate.mli b/contrib/interface/translate.mli
deleted file mode 100644
index 34841fc4..00000000
--- a/contrib/interface/translate.mli
+++ /dev/null
@@ -1,12 +0,0 @@
-open Ascent;;
-open Evd;;
-open Proof_type;;
-open Environ;;
-open Term;;
-
-val translate_goal : goal -> ct_RULE;;
-val translate_goals : goal list -> ct_RULE_LIST;;
-(* The boolean argument indicates whether names from the environment should *)
-(* be avoided (same interpretation as for prterm_env and ast_of_constr) *)
-val translate_constr : bool -> env -> constr -> ct_FORMULA;;
-val translate_path : int list -> ct_SIGNED_INT_LIST;;