aboutsummaryrefslogtreecommitdiff
path: root/contrib/dp/dp.mli
blob: 871a0631ba803898b91012e40d3f0c76dfee5111 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
open Libnames
open Proof_type

val simplify : tactic
val ergo : tactic
val yices : tactic
val cvc_lite : tactic
val harvey : tactic
val zenon : tactic
val gwhy : tactic

val dp_hint : reference list -> unit
val set_timeout : int -> unit
val set_debug : bool -> unit
val set_trace : bool -> unit