From 076e53c0b5585a37f741bd5a3b564e43c663b22b Mon Sep 17 00:00:00 2001 From: notin Date: Tue, 22 Apr 2008 18:02:54 +0000 Subject: Test que la bibliothèque ZArith est chargée lors d'un appel à simplify, ergo, etc. (cf bug #1831) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10832 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/dp/dp.ml | 49 +++++++++++++++++++++++++------------------------ 1 file 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) -- cgit v1.2.3