diff options
| author | mohring | 2004-03-04 18:33:00 +0000 |
|---|---|---|
| committer | mohring | 2004-03-04 18:33:00 +0000 |
| commit | 0303725f298ab676927d4bbc31662eff0113bf69 (patch) | |
| tree | 02d6fc24e482bf2e6cf47e7005fdc907e74c6d3d /contrib/romega/refl_omega.ml | |
| parent | af1cdf0f7145a85399c7f2092f91569f44b55a6a (diff) | |
Reparation ROmega V8/Omega ZERO/POS/NEG
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5431 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/romega/refl_omega.ml')
| -rw-r--r-- | contrib/romega/refl_omega.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml index 86784186fd..ef68c5873e 100644 --- a/contrib/romega/refl_omega.ml +++ b/contrib/romega/refl_omega.ml @@ -700,7 +700,7 @@ let rec oformula_of_constr env t = | Kapp("Zplus",[t1;t2]) -> binop env (fun x y -> Oplus(x,y)) t1 t2 | Kapp("Zminus",[t1;t2]) ->binop env (fun x y -> Ominus(x,y)) t1 t2 | Kapp("Zmult",[t1;t2]) ->binop env (fun x y -> Omult(x,y)) t1 t2 - | Kapp(("POS"|"NEG"|"ZERO"),_) -> + | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> begin try Oint(recognize_number t) with _ -> Oatom (add_reified_atom t env) end | _ -> @@ -1290,13 +1290,16 @@ let resolution env full_reified_goal systems_list = Tactics.apply (Lazy.force coq_I) let total_reflexive_omega_tactic gl = + if !Options.v7 then Util.error "ROmega does not work in v7 mode"; + try let env = new_environment () in - let reified_goal = reify_gl env gl in - let systems_list = destructurate_hyps reified_goal in + let full_reified_goal = reify_gl env gl in + let systems_list = destructurate_hyps full_reified_goal in if !debug then begin display_systems systems_list end; - resolution env reified_goal systems_list gl + resolution env full_reified_goal systems_list gl + with Omega2.NO_CONTRADICTION -> Util.error "ROmega can't solve this system" (*i let tester = Tacmach.hide_atomic_tactic "TestOmega" test_tactic i*) |