Test que la bibliothèque ZArith est chargée lors d'un appel à simplify, ergo, etc. (cf bug #1831)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10832 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 25 insertions, 24 deletions

diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index b24ba55fb..69946374c 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -779,33 +779,34 @@ let ergo_proof_from_file f gl =
 
 let call_prover prover q =
   let fwhy = Filename.temp_file "coq_dp" ".why" in
-  Dp_why.output_file fwhy q;
-  if !debug then Format.eprintf "Why file: %s@." fwhy;
-  match prover with
-    | Simplify -> call_simplify fwhy
-    | Ergo -> call_ergo fwhy
-    | Yices -> call_yices fwhy
-    | Zenon -> call_zenon fwhy
-    | CVCLite -> call_cvcl fwhy
-    | Harvey -> call_harvey fwhy
-    | Gwhy -> call_gwhy fwhy
+    Dp_why.output_file fwhy q;
+    if !debug then Format.eprintf "Why file: %s@." fwhy;
+    match prover with
+      | Simplify -> call_simplify fwhy
+      | Ergo -> call_ergo fwhy
+      | Yices -> call_yices fwhy
+      | Zenon -> call_zenon fwhy
+      | CVCLite -> call_cvcl fwhy
+      | Harvey -> call_harvey fwhy
+      | Gwhy -> call_gwhy fwhy
   
 let dp prover gl =
+  Coqlib.check_required_library(["Coq";"ZArith";"ZArith"]);
   let concl_type = pf_type_of gl (pf_concl gl) in
-  if not (is_Prop concl_type) then error "Conclusion is not a Prop";
-  try 
-    let q = tr_goal gl in
-    begin match call_prover prover q with
-      | Valid (Some f) when prover = Zenon -> Dp_zenon.proof_from_file f gl
-      | Valid (Some f) when prover = Ergo -> ergo_proof_from_file f gl
-      | Valid _ -> Tactics.admit_as_an_axiom gl
-      | Invalid -> error "Invalid"
-      | DontKnow -> error "Don't know"
-      | Timeout -> error "Timeout"
-      | NoAnswer -> Tacticals.tclIDTAC gl
-    end
-  with NotFO ->
-    error "Not a first order goal"
+    if not (is_Prop concl_type) then error "Conclusion is not a Prop";
+    try 
+      let q = tr_goal gl in
+	begin match call_prover prover q with
+	  | Valid (Some f) when prover = Zenon -> Dp_zenon.proof_from_file f gl
+	  | Valid (Some f) when prover = Ergo -> ergo_proof_from_file f gl
+	  | Valid _ -> Tactics.admit_as_an_axiom gl
+	  | Invalid -> error "Invalid"
+	  | DontKnow -> error "Don't know"
+	  | Timeout -> error "Timeout"
+	  | NoAnswer -> Tacticals.tclIDTAC gl
+	end
+    with NotFO ->
+      error "Not a first order goal"
   
 
 let simplify = tclTHEN intros (dp Simplify)