diff options
Diffstat (limited to 'contrib/interface/translate.mli')
| -rw-r--r-- | contrib/interface/translate.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/interface/translate.mli b/contrib/interface/translate.mli index 65d8331b2d..9f25ce38a4 100644 --- a/contrib/interface/translate.mli +++ b/contrib/interface/translate.mli @@ -6,6 +6,6 @@ open Term;; val translate_goal : goal -> ct_RULE;; (* The boolean argument indicates whether names from the environment should *) -(* be avoided (same interpretation as for prterm_env and ast_of_constr) *) +(* be avoided (same interpretation as for pr_lconstr_env and ast_of_constr) *) val translate_constr : bool -> env -> constr -> ct_FORMULA;; val translate_path : int list -> ct_SIGNED_INT_LIST;; |