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
|
