blob: f40f868856d9f75e6bc20825a787c8a24c012214 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
open Libnames
open Proof_type
val simplify : tactic
val ergo : tactic
val cvc3 : tactic
val yices : tactic
val cvc_lite : tactic
val harvey : tactic
val zenon : tactic
val gwhy : tactic
val z3: tactic
val dp_hint : reference list -> unit
val dp_timeout : int -> unit
val dp_debug : bool -> unit
val dp_trace : bool -> unit
val dp_prelude : string list -> unit
val dp_predefined : reference -> string -> unit
|
