diff options
Diffstat (limited to 'contrib/interface/xlate.mli')
| -rw-r--r-- | contrib/interface/xlate.mli | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/contrib/interface/xlate.mli b/contrib/interface/xlate.mli index 0e9fd223fa..6109816b5c 100644 --- a/contrib/interface/xlate.mli +++ b/contrib/interface/xlate.mli @@ -2,13 +2,11 @@ open Ascent;; val xlate_vernac : Vernacexpr.vernac_expr -> ct_COMMAND;; val xlate_tactic : Tacexpr.raw_tactic_expr -> ct_TACTIC_COM;; -val xlate_formula : Ctast.t -> ct_FORMULA;; +val xlate_formula : Topconstr.constr_expr -> ct_FORMULA;; val xlate_int : Ctast.t -> ct_INT;; val xlate_string : Ctast.t -> ct_STRING;; val xlate_ident : Names.identifier -> ct_ID;; val xlate_vernac_list : Vernacexpr.vernac_expr -> ct_COMMAND_LIST;; -val g_nat_syntax_flag : bool ref;; -val set_flags : (unit -> unit) ref;; val set_xlate_mut_stuff : (Ctast.t -> Ctast.t) -> unit;; val declare_in_coq : (unit -> unit);; |