aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/dp/dp_why.mli
blob: 0efa24a2380ee664487876a2838a6dd12aebcb64 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

open Fol

(* generation of the Why file *)

val output_file : string -> query -> unit

(* table to translate the proofs back to Coq (used in dp_zenon) *)

type proof =
  | Immediate of Term.constr
  | Fun_def of string * (string * typ) list * typ * term

val add_proof : proof -> string
val find_proof : string -> proof