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 dc2b2734c..f556c1926 100644 --- a/contrib/interface/dad.mli +++ b/contrib/interface/dad.mli @@ -1,10 +1,10 @@ open Proof_type;; open Tacmach;; - +open Topconstr;; val dad_rule_names : unit -> string list;; val start_dad : unit -> unit;; 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) -> +val add_dad_rule : string -> constr_expr -> (int list) -> (int list) -> int -> (int list) -> Tacexpr.raw_atomic_tactic_expr -> unit;; |