diff options
Diffstat (limited to 'contrib/interface/dad.mli')
| -rw-r--r-- | contrib/interface/dad.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/interface/dad.mli b/contrib/interface/dad.mli index 9f8f7354b..dc2b2734c 100644 --- a/contrib/interface/dad.mli +++ b/contrib/interface/dad.mli @@ -4,7 +4,7 @@ open Tacmach;; val dad_rule_names : unit -> string list;; val start_dad : unit -> unit;; -val dad_tac : (Ctast.t -> 'a) -> tactic_arg list -> goal sigma -> +val dad_tac : (Tacexpr.raw_tactic_expr -> 'a) -> int list -> int list -> goal sigma -> goal list sigma * validation;; val add_dad_rule : string -> Ctast.t -> (int list) -> (int list) -> - int -> (int list) -> Ctast.t -> unit;; + int -> (int list) -> Tacexpr.raw_atomic_tactic_expr -> unit;; |