blob: 9f8f7354b220e5904f3bd1b46613c781c51565f3 (
plain)
1
2
3
4
5
6
7
8
9
10
|
open Proof_type;;
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 ->
goal list sigma * validation;;
val add_dad_rule : string -> Ctast.t -> (int list) -> (int list) ->
int -> (int list) -> Ctast.t -> unit;;
|
