Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 17 insertions, 0 deletions

diff --git a/contrib/dp/dp_why.mli b/contrib/dp/dp_why.mli
new file mode 100644
index 00000000..b38a3d37
--- /dev/null
+++ b/contrib/dp/dp_why.mli
@@ -0,0 +1,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
+
+