diff options
| -rw-r--r-- | contrib/omega/coq_omega.ml | 6 | ||||
| -rw-r--r-- | contrib/romega/const_omega.ml | 11 | ||||
| -rw-r--r-- | contrib/romega/refl_omega.ml | 11 |
3 files changed, 15 insertions, 13 deletions
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index 3ab5a6255a..110a64a058 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -156,9 +156,9 @@ let constant = 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 (if !Options.v7 then "ZERO" else "Z0")) +let coq_POS = lazy (constant (if !Options.v7 then "POS" else "Zpos")) +let coq_NEG = lazy (constant (if !Options.v7 then "NEG" else "Zneg")) let coq_Z = lazy (constant "Z") let coq_relation = lazy (constant (if !Options.v7 then "relation" else "comparison")) let coq_SUPERIEUR = lazy (constant "SUPERIEUR") diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml index b896614312..3b2a7d316e 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 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*) |