From ba7d0994f166b7e5a2545af294e01e899b6e20d9 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 27 Mar 2006 14:38:28 +0000
Subject: appel Zenon sans prelude

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8664 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/dp/dp.ml     | 15 ++++++---------
 contrib/dp/dp_why.ml |  2 ++
 contrib/dp/fol.mli   |  1 +
 3 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index 9a0ad2bb6c..af684e6e92 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -26,7 +26,7 @@ open Hipattern
 open Libnames
 open Declarations
 
-let debug = ref true
+let debug = ref false
 
 let logic_dir = ["Coq";"Logic";"Decidable"]
 let coq_modules =
@@ -369,8 +369,7 @@ and axiomatize_body env r id d = match r with
 	      (match d with
 		 | DeclPred (id, _, []) ->
 		     let value = tr_formula tv [] env b in
-		     [id, And (Imp (Fatom (Pred (id, [])), value),
-			       Imp (value, Fatom (Pred (id, []))))]
+		     [id, Iff (Fatom (Pred (id, [])), value)]
 		 | DeclFun (id, _, [], _) ->
 		     let value = tr_term tv [] env b in
 		     [id, Fatom (Eq (Fol.App (id, []), value))]
@@ -420,10 +419,7 @@ and axiomatize_body env r id d = match r with
 			   end
 		       | DeclPred _ ->
 			   let value = tr_formula tv bv env t in
-			   let p = 
-			     And (Imp (Fatom (Pred (id, fol_vars)), value),
-				  Imp (value, Fatom (Pred (id, fol_vars))))
-			   in
+			   let p = Iff (Fatom (Pred (id, fol_vars)), value) in
 			   [id, foralls vars p]
 		       | _ ->
 			   assert false
@@ -655,8 +651,9 @@ let call_simplify fwhy =
   r
 
 let call_zenon fwhy =
-  if Sys.command (sprintf "why --zenon %s" fwhy) <> 0 then
-    anomaly ("call to why --zenon " ^ fwhy ^ " failed; please report");
+  let cmd = sprintf "why --no-prelude --no-zenon-prelude --zenon %s" fwhy in
+  if Sys.command cmd <> 0 then
+    anomaly ("call to " ^ cmd ^ " failed; please report");
   let fznn = Filename.chop_suffix fwhy ".why" ^ "_why.znn" in
   let cmd = 
     sprintf "timeout 10 zenon %s > out 2>&1 && grep -q PROOF-FOUND out" fznn
diff --git a/contrib/dp/dp_why.ml b/contrib/dp/dp_why.ml
index 662a5a8be6..e1ddb039bd 100644
--- a/contrib/dp/dp_why.ml
+++ b/contrib/dp/dp_why.ml
@@ -77,6 +77,8 @@ let rec print_predicate fmt p =
       fprintf fmt "@[%a(%a)@]" ident id print_terms tl
   | Imp (a, b) ->
       fprintf fmt "@[(%a ->@ %a)@]" pp a pp b
+  | Iff (a, b) ->
+      fprintf fmt "@[(%a <->@ %a)@]" pp a pp b
   | And (a, b) ->
       fprintf fmt "@[(%a and@ %a)@]" pp a pp b
   | Or (a, b) ->
diff --git a/contrib/dp/fol.mli b/contrib/dp/fol.mli
index 5dd46b0d1f..a85469cc67 100644
--- a/contrib/dp/fol.mli
+++ b/contrib/dp/fol.mli
@@ -24,6 +24,7 @@ and atom =
 and form = 
   | Fatom of atom
   | Imp of form * form
+  | Iff of form * form
   | And of form * form
   | Or of form * form
   | Not of form
-- 
cgit v1.2.3