diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-03-29 23:16:06 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-24 17:59:20 +0200 |
commit | 1ef92c718ece547826f4c7e5c1ce78a6965e1ca6 (patch) | |
tree | af3b774894e26419f496d92af7acfadc6466e247 /plugins/romega/refl_omega.ml | |
parent | 0cc7ed04a6a6db666da08a724df3998c1e4888f9 (diff) |
Removing trivial compatibility layer in refl_omega.
Diffstat (limited to 'plugins/romega/refl_omega.ml')
-rw-r--r-- | plugins/romega/refl_omega.ml | 29 |
1 files changed, 15 insertions, 14 deletions
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index cfe14b230..a20589fb4 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -8,6 +8,7 @@ open Pp open Util +open Proofview.Notations open Const_omega module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint) open OmegaSolver @@ -16,13 +17,12 @@ open OmegaSolver (* Especially useful debugging functions *) let debug = ref false -let show_goal gl = - if !debug then (); Tacticals.tclIDTAC gl +let show_goal = Tacticals.New.tclIDTAC let pp i = print_int i; print_newline (); flush stdout (* More readable than the prefix notation *) -let (>>) = Tacticals.tclTHEN +let (>>) = Tacticals.New.tclTHEN let mkApp = Term.mkApp @@ -739,7 +739,7 @@ and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c = (* Destructuration des hypothèses et de la conclusion *) let reify_gl env gl = - let concl = Tacmach.pf_concl gl in + let concl = Tacmach.New.pf_concl gl in let concl = EConstr.Unsafe.to_constr concl in let t_concl = Pnot (oproposition_of_constr env (true,[],id_concl,[O_mono]) gl concl) in @@ -760,7 +760,7 @@ let reify_gl env gl = | [] -> if !debug then print_env_reification env; [] in - let t_lhyps = loop (Tacmach.pf_hyps_types gl) in + let t_lhyps = loop (Tacmach.New.pf_hyps_types gl) in (id_concl,t_concl) :: t_lhyps let rec destructurate_pos_hyp orig list_equations list_depends = function @@ -1283,21 +1283,22 @@ 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 - Proofview.V82.of_tactic (Tactics.generalize - (l_generalize_arg @ List.map EConstr.mkVar (List.tl l_hyps))) >> - Proofview.V82.of_tactic (Tactics.change_concl reified) >> - Proofview.V82.of_tactic (Tactics.apply (EConstr.of_constr (app coq_do_omega [|decompose_tactic; normalization_trace|]))) >> + Tactics.generalize + (l_generalize_arg @ List.map EConstr.mkVar (List.tl l_hyps)) >> + Tactics.change_concl reified >> + Tactics.apply (EConstr.of_constr (app coq_do_omega [|decompose_tactic; normalization_trace|])) >> show_goal >> - Proofview.V82.of_tactic (Tactics.normalise_vm_in_concl) >> + Tactics.normalise_vm_in_concl >> (*i Alternatives to the previous line: - Normalisation without VM: Tactics.normalise_in_concl - Skip the conversion check and rely directly on the QED: Tacmach.convert_concl_no_check (Lazy.force coq_True) Term.VMcast >> i*) - Proofview.V82.of_tactic (Tactics.apply (EConstr.of_constr (Lazy.force coq_I))) + Tactics.apply (EConstr.of_constr (Lazy.force coq_I)) -let total_reflexive_omega_tactic gl = +let total_reflexive_omega_tactic = + Proofview.Goal.nf_enter { enter = begin fun gl -> Coqlib.check_required_library ["Coq";"romega";"ROmega"]; rst_omega_eq (); rst_omega_var (); @@ -1306,9 +1307,9 @@ let total_reflexive_omega_tactic gl = let full_reified_goal = reify_gl env gl in let systems_list = destructurate_hyps full_reified_goal in if !debug then display_systems systems_list; - resolution env full_reified_goal systems_list gl + resolution env full_reified_goal systems_list with NO_CONTRADICTION -> CErrors.error "ROmega can't solve this system" - + end } (*i let tester = Tacmach.hide_atomic_tactic "TestOmega" test_tactic i*) |