diff options
author | 2012-03-02 22:30:29 +0000 | |
---|---|---|
committer | 2012-03-02 22:30:29 +0000 | |
commit | 401f17afa2e9cc3f2d734aef0d71a2c363838ebd (patch) | |
tree | 7a3e0ce211585d4c09a182aad1358dfae0fb38ef /plugins/romega | |
parent | 15cb1aace0460e614e8af1269d874dfc296687b0 (diff) |
Noise for nothing
Util only depends on Ocaml stdlib and Utf8 tables.
Generic pretty printing and loc functions are in Pp.
Generic errors are in Errors.
+ Training white-spaces, useless open, prlist copies random erasure.
Too many "open Errors" on the contrary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/romega')
-rw-r--r-- | plugins/romega/const_omega.ml | 2 | ||||
-rw-r--r-- | plugins/romega/g_romega.ml4 | 2 | ||||
-rw-r--r-- | plugins/romega/refl_omega.ml | 13 |
3 files changed, 9 insertions, 8 deletions
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index e810e15c1..298b24850 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -39,7 +39,7 @@ let destructurate t = | Term.Var id,[] -> Kvar(Names.string_of_id id) | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body) | Term.Prod (Names.Name _,_,_),[] -> - Util.error "Omega: Not a quantifier-free goal" + Errors.error "Omega: Not a quantifier-free goal" | _ -> Kufo exception Destruct diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 2db86e005..87e42354b 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -18,7 +18,7 @@ let romega_tactic l = | "positive" -> Tacinterp.interp <:tactic<zify_positive>> | "N" -> Tacinterp.interp <:tactic<zify_N>> | "Z" -> Tacinterp.interp <:tactic<zify_op>> - | s -> Util.error ("No ROmega knowledge base for type "^s)) + | s -> Errors.error ("No ROmega knowledge base for type "^s)) (Util.list_uniquize (List.sort compare l)) in tclTHEN diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 4a6d462ec..550a4af2b 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -6,6 +6,7 @@ *************************************************************************) +open Errors open Util open Const_omega module OmegaSolver = Omega.MakeOmegaSolver (Bigint) @@ -450,7 +451,7 @@ let rec scalar n = function | Omult(t1,Oint x) -> do_list [Lazy.force coq_c_mult_assoc_reduced], Omult(t1,Oint (n*x)) | Omult(t1,t2) -> - Util.error "Omega: Can't solve a goal with non-linear products" + Errors.error "Omega: Can't solve a goal with non-linear products" | (Oatom _ as t) -> do_list [], Omult(t,Oint n) | Oint i -> do_list [Lazy.force coq_c_reduce],Oint(n*i) | (Oufo _ as t)-> do_list [], Oufo (Omult(t,Oint n)) @@ -469,7 +470,7 @@ let rec negate = function | Omult(t1,Oint x) -> do_list [Lazy.force coq_c_opp_mult_r], Omult(t1,Oint (Bigint.neg x)) | Omult(t1,t2) -> - Util.error "Omega: Can't solve a goal with non-linear products" + Errors.error "Omega: Can't solve a goal with non-linear products" | (Oatom _ as t) -> do_list [Lazy.force coq_c_opp_one], Omult(t,Oint(negone)) | Oint i -> do_list [Lazy.force coq_c_reduce] ,Oint(Bigint.neg i) @@ -541,7 +542,7 @@ let shrink_pair f1 f2 = Lazy.force coq_c_red4, Omult(Oatom v,Oplus(c1,c2)) | t1,t2 -> oprint stdout t1; print_newline (); oprint stdout t2; print_newline (); - flush Pervasives.stdout; Util.error "shrink.1" + flush Pervasives.stdout; Errors.error "shrink.1" end (* \subsection{Calcul d'une sous formule constante} *) @@ -555,9 +556,9 @@ let reduce_factor = function let rec compute = function Oint n -> n | Oplus(t1,t2) -> compute t1 + compute t2 - | _ -> Util.error "condense.1" in + | _ -> Errors.error "condense.1" in [Lazy.force coq_c_reduce], Omult(Oatom v,Oint(compute c)) - | t -> Util.error "reduce_factor.1" + | t -> Errors.error "reduce_factor.1" (* \subsection{Réordonnancement} *) @@ -1291,7 +1292,7 @@ let total_reflexive_omega_tactic gl = let systems_list = destructurate_hyps full_reified_goal in if !debug then display_systems systems_list; resolution env full_reified_goal systems_list gl - with NO_CONTRADICTION -> Util.error "ROmega can't solve this system" + with NO_CONTRADICTION -> Errors.error "ROmega can't solve this system" (*i let tester = Tacmach.hide_atomic_tactic "TestOmega" test_tactic i*) |