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

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*)