diff options
Diffstat (limited to 'plugins/romega/refl_omega.ml')
| -rw-r--r-- | plugins/romega/refl_omega.ml | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 560e6a89..ba882e39 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -9,7 +9,7 @@ open Pp open Util open Const_omega -module OmegaSolver = Omega.MakeOmegaSolver (Bigint) +module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint) open OmegaSolver (* \section{Useful functions and flags} *) @@ -172,7 +172,7 @@ let print_env_reification env = in let prop_info = str "ENVIRONMENT OF PROPOSITIONS :" ++ fnl () ++ loop 'P' 0 env.props in let term_info = str "ENVIRONMENT OF TERMS :" ++ fnl () ++ loop 'V' 0 env.terms in - msg_debug (prop_info ++ fnl () ++ term_info) + Feedback.msg_debug (prop_info ++ fnl () ++ term_info) (* \subsection{Gestion des environnements de variable pour Omega} *) (* generation d'identifiant d'equation pour Omega *) @@ -454,7 +454,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) -> - Errors.error "Omega: Can't solve a goal with non-linear products" + CErrors.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)) @@ -473,7 +473,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) -> - Errors.error "Omega: Can't solve a goal with non-linear products" + CErrors.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) @@ -545,7 +545,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; Errors.error "shrink.1" + flush Pervasives.stdout; CErrors.error "shrink.1" end (* \subsection{Calcul d'une sous formule constante} *) @@ -559,9 +559,9 @@ let reduce_factor = function let rec compute = function Oint n -> n | Oplus(t1,t2) -> compute t1 + compute t2 - | _ -> Errors.error "condense.1" in + | _ -> CErrors.error "condense.1" in [Lazy.force coq_c_reduce], Omult(Oatom v,Oint(compute c)) - | t -> Errors.error "reduce_factor.1" + | t -> CErrors.error "reduce_factor.1" (* \subsection{Réordonnancement} *) @@ -1280,12 +1280,12 @@ let resolution env full_reified_goal systems_list = CCHyp{o_hyp=id_concl;o_path=[]} :: hyp_stated_vars @ initial_context in let decompose_tactic = decompose_tree env context solution_tree in - Tactics.generalize - (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps)) >> + Proofview.V82.of_tactic (Tactics.generalize + (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps))) >> Proofview.V82.of_tactic (Tactics.change_concl reified) >> Proofview.V82.of_tactic (Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|])) >> show_goal >> - Tactics.normalise_vm_in_concl >> + Proofview.V82.of_tactic (Tactics.normalise_vm_in_concl) >> (*i Alternatives to the previous line: - Normalisation without VM: Tactics.normalise_in_concl @@ -1304,7 +1304,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 -> Errors.error "ROmega can't solve this system" + with NO_CONTRADICTION -> CErrors.error "ROmega can't solve this system" (*i let tester = Tacmach.hide_atomic_tactic "TestOmega" test_tactic i*) |