diff options
| author |  mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-04 18:33:00 +0000 |
|---|---|---|
| committer | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-04 18:33:00 +0000 |
| commit | 0303725f298ab676927d4bbc31662eff0113bf69 (patch) | |
| tree | 02d6fc24e482bf2e6cf47e7005fdc907e74c6d3d /contrib/romega | |
| 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')
| -rw-r--r-- | contrib/romega/const_omega.ml | 11 | ||||
| -rw-r--r-- | contrib/romega/refl_omega.ml | 11 |
2 files changed, 12 insertions, 10 deletions
diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml index b89661431..3b2a7d316 100644 --- a/contrib/romega/const_omega.ml +++ b/contrib/romega/const_omega.ml @@ -59,7 +59,7 @@ let recognize_number t = | _ -> failwith "not a number" in let f,l = dest_const_apply t in match Names.string_of_id f,l with - "POS",[t] -> loop t | "NEG",[t] -> - (loop t) | "ZERO",[] -> 0 + "Zpos",[t] -> loop t | "Zneg",[t] -> - (loop t) | "Z0",[] -> 0 | _ -> failwith "not a number";; @@ -77,12 +77,11 @@ let constant = Coqlib.gen_constant_in_modules "Omega" coq_modules let coq_xH = lazy (constant "xH") let coq_xO = lazy (constant "xO") let coq_xI = lazy (constant "xI") -let coq_ZERO = lazy (constant "ZERO") -let coq_POS = lazy (constant "POS") -let coq_NEG = lazy (constant "NEG") +let coq_ZERO = lazy (constant "Z0") +let coq_POS = lazy (constant "Zpos") +let coq_NEG = lazy (constant "Zneg") let coq_Z = lazy (constant "Z") -let coq_relation = lazy (constant (if !Options.v7 then "relation" else "comparis -on")) +let coq_relation = lazy (constant "comparison") let coq_SUPERIEUR = lazy (constant "SUPERIEUR") let coq_INFEEIEUR = lazy (constant "INFERIEUR") let coq_EGAL = lazy (constant "EGAL") diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml index 86784186f..ef68c5873 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*) |