Remplacement du coeur d'omega (omega.ml) par la version plus gnrale utilise par romega (omega2.ml, qui, l'occassion, disparat sous ce nom)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6511 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 245 insertions, 899 deletions

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 86c0640987..8d018bd042 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -56,16 +56,6 @@ let write f x = f:=x
 
 open Goptions
 
-(* Obsolete, subsumed by Time Omega
-let _ =
-  declare_bool_option 
-    { optsync  = false;
-      optname  = "Omega time displaying flag";
-      optkey   = SecondaryTable ("Omega","Time");
-      optread  = read display_time_flag;
-      optwrite = write display_time_flag }
-*)
-
 let _ =
   declare_bool_option 
     { optsync  = false;
@@ -110,6 +100,31 @@ let new_identifier_var =
   let cpt = ref 0 in 
   (fun () -> let s = "Zvar" ^ string_of_int !cpt in incr cpt; id_of_string s)
 
+let new_id =
+  let cpt = ref 0 in fun () -> incr cpt; !cpt
+
+let new_var_num =
+  let cpt = ref 1000 in (fun () -> incr cpt; !cpt)
+
+let new_var =
+  let cpt = ref 0 in fun () -> incr cpt; Nameops.make_ident "WW" (Some !cpt)
+
+let display_var i = Printf.sprintf "O%d" i
+
+let intern_id,unintern_id =
+  let cpt = ref 0 in
+  let table = Hashtbl.create 7 and co_table = Hashtbl.create 7 in
+  (fun (name : identifier) -> 
+     try Hashtbl.find table name with Not_found -> 
+       let idx = !cpt in
+       Hashtbl.add table name idx; 
+       Hashtbl.add co_table idx name;
+       incr cpt; idx),
+  (fun idx -> 
+     try Hashtbl.find co_table idx with Not_found -> 
+       let v = new_var () in
+       Hashtbl.add table v idx; Hashtbl.add co_table idx v; v)
+    
 let mk_then = tclTHENLIST
 
 let exists_tac c = constructor_tac (Some 1) 1 (Rawterm.ImplicitBindings [c])
@@ -848,14 +863,14 @@ let rec negate p = function
   | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zopp, [| c |]))
       
 let rec transform p t = 
-  let default () =
+  let default isnat t' =
     try 
-      let v,th,_ = find_constr t in
+      let v,th,_ = find_constr t' in
       [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v
     with _ -> 
       let v = new_identifier_var ()
       and th = new_identifier () in
-      hide_constr t v th false;
+      hide_constr t' v th isnat;
       [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v
   in
   try match destructurate_term t with
@@ -884,26 +899,18 @@ let rec transform p t =
 	       clever_rewrite p [[P_APP 1];[P_APP 2]] 
 		 (Lazy.force coq_fast_Zmult_sym) in
              let tac,t' = scalar p n t2' in tac1 @ tac2 @ (sym :: tac),t'
-         | _ -> default ()
+         | _ -> default false t
        end
    | Kapp((POS|NEG|ZERO),_) -> 
-       (try ([],Oz(recognize_number t)) with _ -> default ())
+       (try ([],Oz(recognize_number t)) with _ -> default false t)
    | Kvar s -> [],Oatom s
    | Kapp(Zopp,[t]) ->
        let tac,t' = transform (P_APP 1 :: p) t in
        let tac',t'' = negate p t' in
        tac @ tac', t''
-   | Kapp(Inject_nat,[t']) ->
-       begin try 
-         let v,th,_ = find_constr t' in 
-         [clever_rewrite_base p (mkVar v) (mkVar th)],Oatom v
-       with _ -> 
-         let v = new_identifier_var () and th = new_identifier () in
-         hide_constr t' v th true;
-         [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v
-       end
-   | _ -> default ()
-  with e when catchable_exception e -> default ()
+   | Kapp(Inject_nat,[t']) -> default true t'
+   | _ -> default false t
+  with e when catchable_exception e -> default false t
       
 let shrink_pair p f1 f2 =
   match f1,f2 with
@@ -1184,13 +1191,13 @@ let replay_history tactic_normalisation =
 	      (loop l) ];
             tclTHEN (mk_then tac) reflexivity]
 	    
-      | STATE(new_eq,def,orig,m,sigma) :: l ->
+      | STATE {st_new_eq=e;st_def=def;st_orig=orig;st_coef=m;st_var=v} :: l ->
 	  let id = new_identifier () 
 	  and id2 = hyp_of_tag orig.id in
-	  tag_hypothesis id new_eq.id;
+	  tag_hypothesis id e.id;
 	  let eq1 = val_of(decompile def) 
 	  and eq2 = val_of(decompile orig) in
-	  let vid = unintern_id sigma in
+	  let vid = unintern_id v in
 	  let theorem =
             mkApp (build_coq_ex (), [| 
 		      Lazy.force coq_Z;
@@ -1206,7 +1213,7 @@ let replay_history tactic_normalisation =
             clever_rewrite (P_APP 1 :: P_APP 1 :: P_APP 2 :: p_initial) 
               [[P_APP 1]] (Lazy.force coq_fast_Zopp_one) ::
             shuffle_mult_right p_initial
-              orig.body m ({c= -1;v=sigma}::def.body) in
+              orig.body m ({c= -1;v= v}::def.body) in
 	  tclTHENS 
 	    (cut theorem)  
 	    [tclTHENLIST [
@@ -1362,7 +1369,7 @@ let destructure_omega gl tac_def (id,c) =
 let reintroduce id =
   (* [id] cannot be cleared if dependent: protect it by a try *)
   tclTHEN (tclTRY (clear [id])) (intro_using id)
-      
+
 let coq_omega gl =
   clear_tables ();
   let tactic_normalisation, system = 
@@ -1393,17 +1400,19 @@ let coq_omega gl =
       (tclIDTAC,[]) (dump_tables ())
   in
   let system = system @ sys in
-  if !display_system_flag then display_system system;
+  if !display_system_flag then display_system display_var system;
   if !old_style_flag then begin
-    try let _ = simplify false system in tclIDTAC gl
+    try 
+      let _ = simplify (new_id,new_var_num,display_var) false system in
+      tclIDTAC gl
     with UNSOLVABLE -> 
       let _,path = depend [] [] (history ()) in
-      if !display_action_flag then display_action path;
+      if !display_action_flag then display_action display_var path;
       (tclTHEN prelude (replay_history tactic_normalisation path)) gl 
   end else begin 
     try
-      let path = simplify_strong system in
-      if !display_action_flag then display_action path; 
+      let path = simplify_strong (new_id,new_var_num,display_var) system in
+      if !display_action_flag then display_action display_var path; 
       (tclTHEN prelude (replay_history tactic_normalisation path)) gl
     with NO_CONTRADICTION -> error "Omega can't solve this system"
   end
diff --git a/contrib/omega/omega.ml b/contrib/omega/omega.ml
index f6d0b81078..0239bbe736 100755
--- a/contrib/omega/omega.ml
+++ b/contrib/omega/omega.ml
@@ -11,12 +11,12 @@
 (*                                                                        *)
 (* Pierre Crégut (CNET, Lannion, France)                                  *)
 (*                                                                        *)
+(* 13/10/2002 : modified to cope with an external numbering of equations  *)
+(*   and hypothesis. Its use for Omega is not more complex and it makes   *)
+(*   things much simpler for the reflexive version where we should limit  *)
+(*   the number of source of numbering.                                   *)
 (**************************************************************************)
 
-(* $Id$ *) 
-
-open Util
-open Hashtbl
 open Names
 
 let flat_map f =
@@ -47,15 +47,6 @@ let floor_div a b =
     | true, false -> (a-1) / b - 1
     | false,true  -> (a+1) / b - 1
 
-let new_id =
-  let cpt = ref 0 in fun () -> incr cpt; ! cpt
-
-let new_var =
-  let cpt = ref 0 in fun () -> incr cpt; Nameops.make_ident "WW" (Some !cpt)
-    
-let new_var_num =
-  let cpt = ref 1000 in (fun () -> incr cpt; !cpt)
-					  
 type coeff = {c: int ; v: int}
 
 type linear = coeff list
@@ -72,13 +63,20 @@ type afine = {
   (* a constant *)
   constant: int }
 
+type state_action = {
+  st_new_eq : afine;
+  st_def    :  afine;
+  st_orig   : afine;
+  st_coef   : int;
+  st_var    : int }
+
 type action =
   | DIVIDE_AND_APPROX of afine * afine * int * int
   | NOT_EXACT_DIVIDE of afine * int
   | FORGET_C of int
   | EXACT_DIVIDE of afine * int
   | SUM of int * (int * afine) * (int * afine)
-  | STATE of afine * afine * afine * int * int
+  | STATE of state_action 
   | HYP of afine
   | FORGET   of int * int
   | FORGET_I of int * int
@@ -95,18 +93,7 @@ exception UNSOLVABLE
 
 exception NO_CONTRADICTION
 
-let intern_id,unintern_id =
-  let cpt = ref 0 in
-  let table = create 7 and co_table = create 7 in
-  (fun (name : identifier) -> 
-     try find table name with Not_found -> 
-       let idx = !cpt in
-       add table name idx; add co_table idx name; incr cpt; idx),
-  (fun idx -> 
-     try find co_table idx with Not_found -> 
-       let v = new_var () in add table v idx; add co_table idx v; v)
-
-let display_eq (l,e) =
+let display_eq print_var (l,e) =
   let _ = 
     List.fold_left 
       (fun not_first f ->
@@ -114,9 +101,9 @@ let display_eq (l,e) =
 	   (if f.c < 0 then "- " else if not_first then "+ " else "");
 	 let c = abs f.c in
 	 if c = 1 then 
-	   Printf.printf "%s " (string_of_id (unintern_id f.v))
+	   Printf.printf "%s " (print_var f.v)
 	 else 
-	   Printf.printf "%d %s " c (string_of_id (unintern_id f.v)); 
+	   Printf.printf "%d %s " c (print_var f.v); 
 	 true)
       false l
   in
@@ -125,26 +112,33 @@ let display_eq (l,e) =
   else if e < 0 then 
     Printf.printf "- %d " (abs e)
 
+let rec trace_length l =
+  let action_length accu = function
+    | SPLIT_INEQ (_,(_,l1),(_,l2)) ->
+	accu + 1 + trace_length l1 + trace_length l2
+    | _ -> accu + 1 in
+  List.fold_left action_length 0 l
+
 let operator_of_eq = function 
   | EQUA -> "=" | DISE -> "!=" | INEQ -> ">="
 
 let kind_of = function
   | EQUA -> "equation" | DISE -> "disequation" | INEQ -> "inequation"
 
-let display_system l = 
+let display_system print_var l = 
   List.iter 
     (fun { kind=b; body=e; constant=c; id=id} -> 
        print_int id; print_string ": ";
-       display_eq (e,c); print_string (operator_of_eq b);
+       display_eq print_var (e,c); print_string (operator_of_eq b);
        print_string "0\n") 
     l;
   print_string "------------------------\n\n"
 
-let display_inequations l = 
-  List.iter (fun e -> display_eq e;print_string ">= 0\n") l;
+let display_inequations print_var l = 
+  List.iter (fun e -> display_eq print_var e;print_string ">= 0\n") l;
   print_string "------------------------\n\n"
 
-let rec display_action = function
+let rec display_action print_var = function
   | act :: l -> begin match act with
       | DIVIDE_AND_APPROX (e1,e2,k,d) ->
           Printf.printf 
@@ -167,13 +161,13 @@ let rec display_action = function
             "We state %s E%d = %d %s E%d + %d %s E%d.\n" 
             (kind_of e1.kind) e c1 (kind_of e1.kind) e1.id c2 
             (kind_of e2.kind) e2.id
-      | STATE (e,_,_,x,_) ->
+      | STATE { st_new_eq = e; st_coef = x} ->
           Printf.printf "We define a new equation %d :" e.id; 
-          display_eq (e.body,e.constant); 
+          display_eq print_var (e.body,e.constant); 
           print_string (operator_of_eq e.kind); print_string " 0\n"
       | HYP e ->   
           Printf.printf "We define %d :" e.id; 
-          display_eq (e.body,e.constant); 
+          display_eq print_var (e.body,e.constant); 
           print_string (operator_of_eq e.kind); print_string " 0\n"
       | FORGET_C e ->  Printf.printf "E%d is trivially satisfiable.\n" e
       | FORGET (e1,e2) -> Printf.printf "E%d subsumes E%d.\n" e1 e2
@@ -196,19 +190,20 @@ let rec display_action = function
           Printf.printf "inequation E%d states 0 != 0.\n" e
       | SPLIT_INEQ (e,(e1,l1),(e2,l2)) -> 
           Printf.printf "equation E%d is split in E%d and E%d\n\n" e.id e1 e2;
-          display_action l1;
+          display_action print_var l1;
           print_newline ();
-          display_action l2;
+          display_action print_var l2;
           print_newline ()
-    end; display_action l
+    end; display_action print_var l
   | [] -> 
       flush stdout
 
 (*""*)
+let default_print_var v = Printf.sprintf "XX%d" v
 
 let add_event, history, clear_history =
   let accu = ref [] in
-  (fun (v : action) -> if !debug then display_action [v]; push v accu), 
+  (fun (v:action) -> if !debug then display_action default_print_var [v]; push v accu),
   (fun () -> !accu),
   (fun () -> accu := [])
 
@@ -240,8 +235,8 @@ let rec sum p0 p1 = match (p0,p1) with
       else 
 	x2 :: sum l1' l2
 
-let sum_afine eq1 eq2 = 
-  { kind = eq1.kind; id = new_id ();
+let sum_afine new_eq_id eq1 eq2 = 
+  { kind = eq1.kind; id = new_eq_id ();
     body = sum eq1.body eq2.body; constant = eq1.constant + eq2.constant }
 
 exception FACTOR1
@@ -288,81 +283,87 @@ let normalize ({id=id; kind=eq_flag; body=e; constant =x} as eq) =
       [new_eq]
     end else [eq]
 
-let eliminate_with_in {v=v;c=c_unite} eq2
+let eliminate_with_in new_eq_id {v=v;c=c_unite} eq2
                         ({body=e1; constant=c1} as eq1) =
   try
     let (f,_) = chop_var v e1 in 
     let coeff = if c_unite=1 then -f.c else if c_unite= -1 then f.c 
                 else failwith "eliminate_with_in" in
-    let res = sum_afine eq1 (map_eq_afine (fun c -> c * coeff) eq2) in
+    let res = sum_afine new_eq_id eq1 (map_eq_afine (fun c -> c * coeff) eq2) in
     add_event (SUM (res.id,(1,eq1),(coeff,eq2))); res
   with CHOPVAR -> eq1
 
 let omega_mod a b = a - b * floor_div (2 * a + b) (2 * b)
-let banerjee_step original l1 l2 = 
+let banerjee_step (new_eq_id,new_var_id,print_var) original l1 l2 = 
   let e = original.body in
-  let sigma = new_var_num () in
+  let sigma = new_var_id () in
   let smallest,var =
     try
       List.fold_left (fun (v,p) c ->  if v > (abs c.c) then abs c.c,c.v else (v,p))
               (abs (List.hd e).c, (List.hd e).v) (List.tl e)
-    with Failure "tl" -> display_system [original] ; failwith "TL" in
+    with Failure "tl" -> display_system print_var [original] ; failwith "TL" in
   let m = smallest + 1 in
   let new_eq =
     { constant = omega_mod original.constant m;
       body = {c= -m;v=sigma} :: 
              map_eq_linear (fun a -> omega_mod a m) original.body;
-      id = new_id (); kind = EQUA } in
+      id = new_eq_id (); kind = EQUA } in
   let definition =
     { constant = - floor_div (2 * original.constant + m) (2 * m);
       body = map_eq_linear (fun a -> - floor_div (2 * a + m) (2 * m))
                              original.body;
-      id = new_id (); kind = EQUA } in
-  add_event (STATE (new_eq,definition,original,m,sigma));
+      id = new_eq_id (); kind = EQUA } in
+  add_event (STATE {st_new_eq = new_eq; st_def = definition;
+		    st_orig =original; st_coef = m; st_var = sigma});
   let new_eq = List.hd (normalize new_eq) in
   let eliminated_var, def = chop_var var new_eq.body in
   let other_equations = 
-    flat_map (fun e -> normalize (eliminate_with_in eliminated_var new_eq e))
+    flat_map (fun e -> normalize (eliminate_with_in new_eq_id eliminated_var new_eq e))
              l1 in
   let inequations = 
-    flat_map (fun e -> normalize (eliminate_with_in eliminated_var new_eq e))
+    flat_map (fun e -> normalize (eliminate_with_in new_eq_id eliminated_var new_eq e))
              l2 in
-  let original' = eliminate_with_in eliminated_var new_eq original in
+  let original' = eliminate_with_in new_eq_id eliminated_var new_eq original in
   let mod_original = map_eq_afine (fun c -> c / m) original' in
   add_event (EXACT_DIVIDE (original',m));
   List.hd (normalize mod_original),other_equations,inequations
 
-let rec eliminate_one_equation (e,other,ineqs) = 
-  if !debug then display_system (e::other);
+let rec eliminate_one_equation ((new_eq_id,new_var_id,print_var) as new_ids) (e,other,ineqs) = 
+  if !debug then display_system print_var (e::other);
   try
     let v,def = chop_factor_1 e.body in
-    (flat_map (fun e' -> normalize (eliminate_with_in v e e')) other,
-     flat_map (fun e' -> normalize (eliminate_with_in v e e')) ineqs)
-  with FACTOR1 -> eliminate_one_equation (banerjee_step e other ineqs)
+    (flat_map (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) other,
+     flat_map (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) ineqs)
+  with FACTOR1 -> 
+    eliminate_one_equation new_ids (banerjee_step new_ids e other ineqs)
 
-let rec banerjee (sys_eq,sys_ineq) =
+let rec banerjee ((_,_,print_var) as new_ids) (sys_eq,sys_ineq) =
   let rec fst_eq_1 = function
      (eq::l) -> 
         if List.exists (fun x -> abs x.c = 1) eq.body then eq,l
         else let (eq',l') = fst_eq_1 l in (eq',eq::l')
    | [] -> raise Not_found in
   match sys_eq with
-     [] -> if !debug then display_system sys_ineq; sys_ineq
+     [] -> if !debug then display_system print_var sys_ineq; sys_ineq
    | (e1::rest) -> 
        let eq,other = try fst_eq_1 sys_eq with Not_found -> (e1,rest) in
        if eq.body = [] then 
          if eq.constant = 0 then begin
-           add_event (FORGET_C eq.id); banerjee (other,sys_ineq)
+           add_event (FORGET_C eq.id); banerjee new_ids (other,sys_ineq)
          end else begin
            add_event (CONSTANT_NOT_NUL(eq.id,eq.constant)); raise UNSOLVABLE
          end
-       else banerjee (eliminate_one_equation (eq,other,sys_ineq))
+       else
+	 banerjee new_ids 
+	   (eliminate_one_equation new_ids (eq,other,sys_ineq))
+
 type kind = INVERTED | NORMAL
-let redundancy_elimination system =
+
+let redundancy_elimination new_eq_id system =
   let normal = function
      ({body=f::_} as e) when f.c < 0 ->  negate_eq e, INVERTED
    | e -> e,NORMAL in
-  let table = create 7 in
+  let table = Hashtbl.create 7 in
   List.iter
     (fun e -> 
        let ({body=ne} as nx) ,kind = normal e in
@@ -372,7 +373,7 @@ let redundancy_elimination system =
          end else add_event (FORGET_C nx.id)
        else
        try 
-         let (optnormal,optinvert) = find table ne in
+         let (optnormal,optinvert) = Hashtbl.find table ne in
          let final =
            if kind = NORMAL then begin
              match optnormal with 
@@ -400,18 +401,18 @@ let redundancy_elimination system =
                 raise UNSOLVABLE
               end
           | _ -> () end;
-         remove table ne;
-         add table ne final
+         Hashtbl.remove table ne;
+         Hashtbl.add table ne final
        with Not_found ->
-         add table ne 
+         Hashtbl.add table ne 
            (if kind = NORMAL then (Some nx,None) else (None,Some nx)))
     system;
   let accu_eq = ref [] in
   let accu_ineq = ref [] in
-  iter
+  Hashtbl.iter
     (fun p0 p1 -> match (p0,p1) with 
-       | (e, (Some x, Some y)) when x.constant = y.constant ->
-           let id=new_id () in
+       | (e, (Some x, Some y)) when x.constant = y.constant -> 
+           let id=new_eq_id () in
            add_event (MERGE_EQ(id,x,y.id));
            push {id=id; kind=EQUA; body=x.body; constant=x.constant} accu_eq
        | (e, (optnorm,optinvert)) ->
@@ -425,14 +426,14 @@ let redundancy_elimination system =
 exception SOLVED_SYSTEM
 
 let select_variable system =
-  let table = create 7 in
+  let table = Hashtbl.create 7 in
   let push v c= 
-    try let r = find table v in r := max !r (abs c)
-    with Not_found -> add table v (ref (abs c)) in
+    try let r = Hashtbl.find table v in r := max !r (abs c)
+    with Not_found -> Hashtbl.add table v (ref (abs c)) in
   List.iter (fun {body=l} -> List.iter (fun f -> push f.v f.c) l) system;
   let vmin,cmin = ref (-1), ref 0 in
   let var_cpt = ref 0 in
-  iter
+  Hashtbl.iter
     (fun v ({contents =  c}) ->
        incr var_cpt;
        if c < !cmin or !vmin = (-1) then begin vmin := v; cmin := c end)
@@ -449,13 +450,13 @@ let classify v system =
        with CHOPVAR -> (eq::not_occ,below,over))
     ([],[],[]) system
 
-let product dark_shadow low high =
+let product new_eq_id dark_shadow low high =
   List.fold_left
     (fun accu (a,eq1) ->
        List.fold_left
          (fun accu (b,eq2) ->
             let eq = 
-              sum_afine (map_eq_afine (fun c -> c * b) eq1)
+              sum_afine new_eq_id (map_eq_afine (fun c -> c * b) eq1)
                 (map_eq_afine (fun c -> c * a) eq2) in
             add_event(SUM(eq.id,(b,eq1),(a,eq2)));
             match normalize eq with
@@ -473,33 +474,34 @@ let product dark_shadow low high =
          accu high)
     [] low
 
-let fourier_motzkin dark_shadow system =
+let fourier_motzkin (_,new_eq_id,print_var) dark_shadow system =
   let v = select_variable system in
   let (ineq_out, ineq_low,ineq_high) = classify v system in
-  let expanded = ineq_out @ product dark_shadow ineq_low ineq_high in
-  if !debug then display_system expanded; expanded
+  let expanded = ineq_out @ product new_eq_id dark_shadow ineq_low ineq_high in
+  if !debug then display_system print_var expanded; expanded
 
-let simplify dark_shadow system =
+let simplify ((new_eq_id,new_var_id,print_var) as new_ids) dark_shadow system =
   if List.exists (fun e -> e.kind = DISE) system then 
     failwith "disequation in simplify";
   clear_history ();
   List.iter (fun e -> add_event (HYP e)) system;
   let system = flat_map normalize system in
   let eqs,ineqs = filter (fun e -> e.kind=EQUA) system in
-  let simp_eq,simp_ineq = redundancy_elimination ineqs in
+  let simp_eq,simp_ineq = redundancy_elimination new_eq_id ineqs in
   let system = (eqs @ simp_eq,simp_ineq) in
   let rec loop1a system =
-    let sys_ineq = banerjee system in 
+    let sys_ineq = banerjee new_ids system in 
     loop1b sys_ineq 
   and loop1b sys_ineq =
-    let simp_eq,simp_ineq = redundancy_elimination sys_ineq in
+    let simp_eq,simp_ineq = redundancy_elimination new_eq_id sys_ineq in
     if simp_eq = [] then simp_ineq else loop1a (simp_eq,simp_ineq) 
   in
   let rec loop2 system =
     try
-      let expanded = fourier_motzkin dark_shadow system in
+      let expanded = fourier_motzkin new_ids dark_shadow system in
       loop2 (loop1b expanded)
-    with SOLVED_SYSTEM -> if !debug then display_system system; system 
+    with SOLVED_SYSTEM ->
+      if !debug then display_system print_var system; system 
   in
   loop2 (loop1a system)
 
@@ -520,7 +522,7 @@ let rec depend relie_on accu = function
 	      depend (e1.id::e2.id::relie_on) (act::accu) l
             else 
 	      depend relie_on accu l
-	| STATE (e,_,_,_,_) ->
+	| STATE {st_new_eq=e} ->
             if List.mem e.id relie_on then depend relie_on (act::accu) l
             else depend relie_on accu l
 	| HYP e ->   
@@ -546,54 +548,63 @@ let rec depend relie_on accu = function
       end
   | [] -> relie_on, accu
 
-let solve system =
-  try let _ = simplify false system in failwith "no contradiction"
-  with UNSOLVABLE -> display_action (snd (depend [] [] (history ())))
+(*
+let depend relie_on accu trace = 
+  Printf.printf "Longueur de la trace initiale : %d\n" 
+    (trace_length trace + trace_length accu);
+  let rel',trace' = depend relie_on accu trace in
+  Printf.printf "Longueur de la trace simplifiée : %d\n" (trace_length trace');
+  rel',trace'
+*)
+
+let solve (new_eq_id,new_eq_var,print_var) system =
+  try let _ = simplify new_eq_id false system in failwith "no contradiction"
+  with UNSOLVABLE -> display_action print_var (snd (depend [] [] (history ())))
       
 let negation (eqs,ineqs) =
   let diseq,_ = filter (fun e -> e.kind = DISE) ineqs in
   let normal = function
     | ({body=f::_} as e) when f.c < 0 ->  negate_eq e, INVERTED
     | e -> e,NORMAL in
-  let table = create 7 in
+  let table = Hashtbl.create 7 in
   List.iter (fun e -> 
                let {body=ne;constant=c} ,kind = normal e in
-               add table (ne,c) (kind,e)) diseq;
+               Hashtbl.add table (ne,c) (kind,e)) diseq;
   List.iter (fun e ->
-               if e.kind <> EQUA then pp 9999;
+               assert (e.kind <> EQUA);
                let {body=ne;constant=c},kind = normal e in
                try 
-		 let (kind',e') = find table (ne,c) in
+		 let (kind',e') = Hashtbl.find table (ne,c) in
 		 add_event (NEGATE_CONTRADICT (e,e',kind=kind'));
 		 raise UNSOLVABLE
                with Not_found -> ()) eqs
 
 exception FULL_SOLUTION of action list * int list
 
-let simplify_strong system =
+let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system =
   clear_history ();
   List.iter (fun e -> add_event (HYP e)) system;
   (* Initial simplification phase *)
   let rec loop1a system =
     negation system;
-    let sys_ineq = banerjee system in 
+    let sys_ineq = banerjee new_ids system in 
     loop1b sys_ineq 
   and loop1b sys_ineq =
     let dise,ine = filter (fun e -> e.kind = DISE) sys_ineq in
-    let simp_eq,simp_ineq = redundancy_elimination ine in
+    let simp_eq,simp_ineq = redundancy_elimination new_eq_id ine in
     if simp_eq = [] then dise @ simp_ineq
     else loop1a (simp_eq,dise @ simp_ineq) 
   in
   let rec loop2 system =
     try
-      let expanded = fourier_motzkin false system in
+      let expanded = fourier_motzkin new_ids false system in
       loop2 (loop1b expanded)
-    with SOLVED_SYSTEM -> if !debug then display_system system; system 
+    with SOLVED_SYSTEM -> if !debug then display_system print_var system; system 
   in
   let rec explode_diseq = function 
     | (de::diseq,ineqs,expl_map) ->
-	let id1 = new_id () 
-	and id2 = new_id () in
+	let id1 = new_eq_id () 
+	and id2 = new_eq_id () in
 	let e1 = 
 	  {id = id1; kind=INEQ; body = de.body; constant = de.constant - 1} in
 	let e2 = 
@@ -612,7 +623,7 @@ let simplify_strong system =
     let system = flat_map normalize system in
     let eqs,ineqs = filter (fun e -> e.kind=EQUA) system in
     let dise,ine = filter (fun e -> e.kind = DISE) ineqs in
-    let simp_eq,simp_ineq = redundancy_elimination ine in
+    let simp_eq,simp_ineq = redundancy_elimination new_eq_id ine in
     let system = (eqs @ simp_eq,simp_ineq @ dise) in
     let system' = loop1a system in
     let diseq,ineq = filter (fun e -> e.kind = DISE) system' in
@@ -631,14 +642,15 @@ let simplify_strong system =
         sys_exploded 
     in
     let max_count sys = 
-      let tbl = create 7 in
+      let tbl = Hashtbl.create 7 in
       let augment x = 
-        try incr (find tbl x) with Not_found -> add tbl x (ref 1) in
+        try incr (Hashtbl.find tbl x) 
+	with Not_found -> Hashtbl.add tbl x (ref 1) in
       let eq = ref (-1) and c = ref 0 in
       List.iter (function 
 		   | ([],r_on,_,path) -> raise (FULL_SOLUTION (path,r_on))
                    | (l,_,_,_) -> List.iter augment l) sys;
-      iter (fun x v -> if !v > !c then begin eq := x; c := !v end) tbl;
+      Hashtbl.iter (fun x v -> if !v > !c then begin eq := x; c := !v end) tbl;
       !eq 
     in
     let rec solve systems = 
@@ -649,13 +661,13 @@ let simplify_strong system =
           | [] -> failwith "solve" in
         let s1,s2 = filter (fun (_,_,decomp,_) -> sign decomp) systems in
         let s1' = 
-	  List.map (fun (dep,ro,dc,pa) -> (list_except id dep,ro,dc,pa)) s1 in
+	  List.map (fun (dep,ro,dc,pa) -> (Util.list_except id dep,ro,dc,pa)) s1 in
         let s2' = 
-	  List.map (fun (dep,ro,dc,pa) -> (list_except id dep,ro,dc,pa)) s2 in
+	  List.map (fun (dep,ro,dc,pa) -> (Util.list_except id dep,ro,dc,pa)) s2 in
         let (r1,relie1) = solve s1' 
 	and (r2,relie2) = solve s2' in
 	let (eq,id1,id2) = List.assoc id explode_map in
-	[SPLIT_INEQ(eq,(id1,r1),(id2, r2))], eq.id :: list_union relie1 relie2
+	[SPLIT_INEQ(eq,(id1,r1),(id2, r2))], eq.id :: Util.list_union relie1 relie2
       with FULL_SOLUTION (x0,x1) -> (x0,x1) 
     in
     let act,relie_on = solve all_solutions in
diff --git a/contrib/romega/omega2.ml b/contrib/romega/omega2.ml
deleted file mode 100644
index 91aefc60d0..0000000000
--- a/contrib/romega/omega2.ml
+++ /dev/null
@@ -1,675 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-(**************************************************************************)
-(*                                                                        *)
-(* Omega: a solver of quantifier-free problems in Presburger Arithmetic   *)
-(*                                                                        *)
-(* Pierre Crégut (CNET, Lannion, France)                                  *)
-(*                                                                        *)
-(* 13/10/2002 : modified to cope with an external numbering of equations  *)
-(*   and hypothesis. Its use for Omega is not more complex and it makes   *)
-(*   things much simpler for the reflexive version where we should limit  *)
-(*   the number of source of numbering.                                   *)
-(**************************************************************************)
-
-open Names
-
-let flat_map f =
- let rec flat_map_f = function
-   | [] -> [] 
-   | x :: l -> f x @ flat_map_f l
- in 
- flat_map_f
-
-let pp i = print_int i; print_newline (); flush stdout
-
-let debug = ref false
-
-let filter = List.partition
-
-let push v l = l := v :: !l
-
-let rec pgcd x y = if y = 0 then x else pgcd y (x mod y)
-
-let pgcd_l = function
-  | [] -> failwith "pgcd_l"
-  | x :: l -> List.fold_left pgcd x l
-
-let floor_div a b =
-  match a >=0 , b > 0 with
-    | true,true -> a / b
-    | false,false -> a / b
-    | true, false -> (a-1) / b - 1
-    | false,true  -> (a+1) / b - 1
-
-type coeff = {c: int ; v: int}
-
-type linear = coeff list
-
-type eqn_kind = EQUA | INEQ | DISE
-
-type afine = { 
-  (* a number uniquely identifying the equation *)
-  id: int ; 
-  (* a boolean true for an eq, false for an ineq (Sigma a_i x_i >= 0) *)
-  kind: eqn_kind; 
-  (* the variables and their coefficient *)
-  body: coeff list; 
-  (* a constant *)
-  constant: int }
-
-type state_action = {
-  st_new_eq : afine;
-  st_def    :  afine;
-  st_orig   : afine;
-  st_coef   : int;
-  st_var    : int }
-
-type action =
-  | DIVIDE_AND_APPROX of afine * afine * int * int
-  | NOT_EXACT_DIVIDE of afine * int
-  | FORGET_C of int
-  | EXACT_DIVIDE of afine * int
-  | SUM of int * (int * afine) * (int * afine)
-  | STATE of state_action 
-  | HYP of afine
-  | FORGET   of int * int
-  | FORGET_I of int * int
-  | CONTRADICTION of afine * afine
-  | NEGATE_CONTRADICT of afine * afine * bool
-  | MERGE_EQ of int * afine * int 
-  | CONSTANT_NOT_NUL of int * int
-  | CONSTANT_NUL of int
-  | CONSTANT_NEG of int * int
-  | SPLIT_INEQ of afine * (int * action list) * (int * action list)
-  | WEAKEN of int * int
-
-exception UNSOLVABLE
-
-exception NO_CONTRADICTION
-
-let display_eq print_var (l,e) =
-  let _ = 
-    List.fold_left 
-      (fun not_first f ->
-	 print_string 
-	   (if f.c < 0 then "- " else if not_first then "+ " else "");
-	 let c = abs f.c in
-	 if c = 1 then 
-	   Printf.printf "%s " (print_var f.v)
-	 else 
-	   Printf.printf "%d %s " c (print_var f.v); 
-	 true)
-      false l
-  in
-  if e > 0 then 
-    Printf.printf "+ %d " e 
-  else if e < 0 then 
-    Printf.printf "- %d " (abs e)
-
-let rec trace_length l =
-  let action_length accu = function
-    | SPLIT_INEQ (_,(_,l1),(_,l2)) ->
-	accu + 1 + trace_length l1 + trace_length l2
-    | _ -> accu + 1 in
-  List.fold_left action_length 0 l
-
-let operator_of_eq = function 
-  | EQUA -> "=" | DISE -> "!=" | INEQ -> ">="
-
-let kind_of = function
-  | EQUA -> "equation" | DISE -> "disequation" | INEQ -> "inequation"
-
-let display_system print_var l = 
-  List.iter 
-    (fun { kind=b; body=e; constant=c; id=id} -> 
-       print_int id; print_string ": ";
-       display_eq print_var (e,c); print_string (operator_of_eq b);
-       print_string "0\n") 
-    l;
-  print_string "------------------------\n\n"
-
-let display_inequations print_var l = 
-  List.iter (fun e -> display_eq print_var e;print_string ">= 0\n") l;
-  print_string "------------------------\n\n"
-
-let rec display_action print_var = function
-  | act :: l -> begin match act with
-      | DIVIDE_AND_APPROX (e1,e2,k,d) ->
-          Printf.printf 
-            "Inequation E%d is divided by %d and the constant coefficient is \
-            rounded by substracting %d.\n" e1.id k d
-      | NOT_EXACT_DIVIDE (e,k) ->
-          Printf.printf
-            "Constant in equation E%d is not divisible by the pgcd \
-            %d of its other coefficients.\n" e.id k
-      | EXACT_DIVIDE (e,k) ->
-          Printf.printf
-            "Equation E%d is divided by the pgcd \
-            %d of its coefficients.\n" e.id k
-      | WEAKEN (e,k) ->
-          Printf.printf 
-            "To ensure a solution in the dark shadow \
-            the equation E%d is weakened by %d.\n" e k
-      | SUM (e,(c1,e1),(c2,e2)) -> 
-          Printf.printf
-            "We state %s E%d = %d %s E%d + %d %s E%d.\n" 
-            (kind_of e1.kind) e c1 (kind_of e1.kind) e1.id c2 
-            (kind_of e2.kind) e2.id
-      | STATE { st_new_eq = e; st_coef = x} ->
-          Printf.printf "We define a new equation %d :" e.id; 
-          display_eq print_var (e.body,e.constant); 
-          print_string (operator_of_eq e.kind); print_string " 0\n"
-      | HYP e ->   
-          Printf.printf "We define %d :" e.id; 
-          display_eq print_var (e.body,e.constant); 
-          print_string (operator_of_eq e.kind); print_string " 0\n"
-      | FORGET_C e ->  Printf.printf "E%d is trivially satisfiable.\n" e
-      | FORGET (e1,e2) -> Printf.printf "E%d subsumes E%d.\n" e1 e2
-      | FORGET_I (e1,e2) -> Printf.printf "E%d subsumes E%d.\n" e1 e2
-      | MERGE_EQ (e,e1,e2) ->
-         Printf.printf "E%d and E%d can be merged into E%d.\n" e1.id e2 e
-      | CONTRADICTION (e1,e2) -> 
-          Printf.printf
-            "equations E%d and E%d implie a contradiction on their \
-            constant factors.\n" e1.id e2.id
-      | NEGATE_CONTRADICT(e1,e2,b) ->
-          Printf.printf
-            "Eqations E%d and E%d state that their body is at the same time
-            equal and different\n" e1.id e2.id
-      | CONSTANT_NOT_NUL (e,k) -> 
-          Printf.printf "equation E%d states %d=0.\n" e k
-      | CONSTANT_NEG(e,k) -> 
-          Printf.printf "equation E%d states %d >= 0.\n" e k
-      | CONSTANT_NUL e ->
-          Printf.printf "inequation E%d states 0 != 0.\n" e
-      | SPLIT_INEQ (e,(e1,l1),(e2,l2)) -> 
-          Printf.printf "equation E%d is split in E%d and E%d\n\n" e.id e1 e2;
-          display_action print_var l1;
-          print_newline ();
-          display_action print_var l2;
-          print_newline ()
-    end; display_action print_var l
-  | [] -> 
-      flush stdout
-
-(*""*)
-let default_print_var v = Printf.sprintf "XX%d" v
-
-let add_event, history, clear_history =
-  let accu = ref [] in
-  (fun (v:action) -> if !debug then display_action default_print_var [v]; push v accu),
-  (fun () -> !accu),
-  (fun () -> accu := [])
-
-let nf_linear = Sort.list (fun x y -> x.v > y.v)
-
-let nf ((b : bool),(e,(x : int))) = (b,(nf_linear e,x))
-
-let map_eq_linear f = 
-  let rec loop = function
-    | x :: l -> let c = f x.c in if c=0 then loop l else {v=x.v; c=c} :: loop l
-    | [] -> [] 
-  in
-  loop
-
-let map_eq_afine f e = 
-  { id = e.id; kind = e.kind; body = map_eq_linear f e.body; 
-    constant = f e.constant }
-
-let negate_eq = map_eq_afine (fun x -> -x)
-
-let rec sum p0 p1 = match (p0,p1) with 
-  | ([], l) -> l | (l, []) -> l
-  | (((x1::l1) as l1'), ((x2::l2) as l2')) -> 
-      if x1.v = x2.v then
-	let c = x1.c + x2.c in
-	if c = 0 then sum l1 l2 else {v=x1.v;c=c} :: sum l1 l2
-      else if x1.v > x2.v then 
-	x1 :: sum l1 l2'
-      else 
-	x2 :: sum l1' l2
-
-let sum_afine new_eq_id eq1 eq2 = 
-  { kind = eq1.kind; id = new_eq_id ();
-    body = sum eq1.body eq2.body; constant = eq1.constant + eq2.constant }
-
-exception FACTOR1
-
-let rec chop_factor_1 = function
-  | x :: l -> 
-      if abs x.c = 1 then x,l else let (c',l') = chop_factor_1 l in (c',x::l')
-  | [] -> raise FACTOR1
-
-exception CHOPVAR
-
-let rec chop_var v = function
-  | f :: l -> if f.v = v then f,l else let (f',l') = chop_var v l in (f',f::l')
-  | [] -> raise CHOPVAR
-
-let normalize ({id=id; kind=eq_flag; body=e; constant =x} as eq) =
-  if e = [] then begin 
-    match eq_flag with
-      | EQUA ->
-          if x =0 then [] else begin
-            add_event (CONSTANT_NOT_NUL(id,x)); raise UNSOLVABLE
-         end
-      | DISE ->
-          if x <> 0 then [] else begin
-            add_event (CONSTANT_NUL id); raise UNSOLVABLE
-          end
-      | INEQ ->
-          if x >= 0 then [] else begin
-            add_event (CONSTANT_NEG(id,x)); raise UNSOLVABLE
-          end
-  end else
-    let gcd = pgcd_l (List.map (fun f -> abs f.c) e) in
-    if eq_flag=EQUA & x mod gcd <> 0 then begin
-      add_event (NOT_EXACT_DIVIDE (eq,gcd)); raise UNSOLVABLE
-    end else if eq_flag=DISE & x mod gcd <> 0 then begin
-      add_event (FORGET_C eq.id); []
-    end else if gcd <> 1 then begin
-      let c = floor_div x gcd in
-      let d = x - c * gcd in
-      let new_eq = {id=id; kind=eq_flag; constant=c; 
-                    body=map_eq_linear (fun c -> c / gcd) e} in
-      add_event (if eq_flag=EQUA or eq_flag = DISE then EXACT_DIVIDE(eq,gcd)
-                 else DIVIDE_AND_APPROX(eq,new_eq,gcd,d));
-      [new_eq]
-    end else [eq]
-
-let eliminate_with_in new_eq_id {v=v;c=c_unite} eq2
-                        ({body=e1; constant=c1} as eq1) =
-  try
-    let (f,_) = chop_var v e1 in 
-    let coeff = if c_unite=1 then -f.c else if c_unite= -1 then f.c 
-                else failwith "eliminate_with_in" in
-    let res = sum_afine new_eq_id eq1 (map_eq_afine (fun c -> c * coeff) eq2) in
-    add_event (SUM (res.id,(1,eq1),(coeff,eq2))); res
-  with CHOPVAR -> eq1
-
-let omega_mod a b = a - b * floor_div (2 * a + b) (2 * b)
-let banerjee_step (new_eq_id,new_var_id,print_var) original l1 l2 = 
-  let e = original.body in
-  let sigma = new_var_id () in
-  let smallest,var =
-    try
-      List.fold_left (fun (v,p) c ->  if v > (abs c.c) then abs c.c,c.v else (v,p))
-              (abs (List.hd e).c, (List.hd e).v) (List.tl e)
-    with Failure "tl" -> display_system print_var [original] ; failwith "TL" in
-  let m = smallest + 1 in
-  let new_eq =
-    { constant = omega_mod original.constant m;
-      body = {c= -m;v=sigma} :: 
-             map_eq_linear (fun a -> omega_mod a m) original.body;
-      id = new_eq_id (); kind = EQUA } in
-  let definition =
-    { constant = - floor_div (2 * original.constant + m) (2 * m);
-      body = map_eq_linear (fun a -> - floor_div (2 * a + m) (2 * m))
-                             original.body;
-      id = new_eq_id (); kind = EQUA } in
-  add_event (STATE {st_new_eq = new_eq; st_def = definition;
-		    st_orig =original; st_coef = m; st_var = sigma});
-  let new_eq = List.hd (normalize new_eq) in
-  let eliminated_var, def = chop_var var new_eq.body in
-  let other_equations = 
-    flat_map (fun e -> normalize (eliminate_with_in new_eq_id eliminated_var new_eq e))
-             l1 in
-  let inequations = 
-    flat_map (fun e -> normalize (eliminate_with_in new_eq_id eliminated_var new_eq e))
-             l2 in
-  let original' = eliminate_with_in new_eq_id eliminated_var new_eq original in
-  let mod_original = map_eq_afine (fun c -> c / m) original' in
-  add_event (EXACT_DIVIDE (original',m));
-  List.hd (normalize mod_original),other_equations,inequations
-
-let rec eliminate_one_equation ((new_eq_id,new_var_id,print_var) as new_ids) (e,other,ineqs) = 
-  if !debug then display_system print_var (e::other);
-  try
-    let v,def = chop_factor_1 e.body in
-    (flat_map (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) other,
-     flat_map (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) ineqs)
-  with FACTOR1 -> 
-    eliminate_one_equation new_ids (banerjee_step new_ids e other ineqs)
-
-let rec banerjee ((_,_,print_var) as new_ids) (sys_eq,sys_ineq) =
-  let rec fst_eq_1 = function
-     (eq::l) -> 
-        if List.exists (fun x -> abs x.c = 1) eq.body then eq,l
-        else let (eq',l') = fst_eq_1 l in (eq',eq::l')
-   | [] -> raise Not_found in
-  match sys_eq with
-     [] -> if !debug then display_system print_var sys_ineq; sys_ineq
-   | (e1::rest) -> 
-       let eq,other = try fst_eq_1 sys_eq with Not_found -> (e1,rest) in
-       if eq.body = [] then 
-         if eq.constant = 0 then begin
-           add_event (FORGET_C eq.id); banerjee new_ids (other,sys_ineq)
-         end else begin
-           add_event (CONSTANT_NOT_NUL(eq.id,eq.constant)); raise UNSOLVABLE
-         end
-       else
-	 banerjee new_ids 
-	   (eliminate_one_equation new_ids (eq,other,sys_ineq))
-
-type kind = INVERTED | NORMAL
-
-let redundancy_elimination new_eq_id system =
-  let normal = function
-     ({body=f::_} as e) when f.c < 0 ->  negate_eq e, INVERTED
-   | e -> e,NORMAL in
-  let table = Hashtbl.create 7 in
-  List.iter
-    (fun e -> 
-       let ({body=ne} as nx) ,kind = normal e in
-       if ne = [] then
-         if nx.constant < 0 then begin
-           add_event (CONSTANT_NEG(nx.id,nx.constant)); raise UNSOLVABLE
-         end else add_event (FORGET_C nx.id)
-       else
-       try 
-         let (optnormal,optinvert) = Hashtbl.find table ne in
-         let final =
-           if kind = NORMAL then begin
-             match optnormal with 
-                Some v -> 
-                  let kept =
-                    if v.constant < nx.constant 
-                    then begin add_event (FORGET (v.id,nx.id));v end
-                    else begin add_event (FORGET (nx.id,v.id));nx end in
-                  (Some(kept),optinvert)
-              | None -> Some nx,optinvert
-           end else begin
-             match optinvert with 
-                Some v ->
-                  let kept =
-                    if v.constant > nx.constant 
-                    then begin add_event (FORGET_I (v.id,nx.id));v end
-                    else begin add_event (FORGET_I (nx.id,v.id));nx end in
-                  (optnormal,Some(if v.constant > nx.constant then v else nx))
-              | None -> optnormal,Some nx
-           end in
-         begin match final with
-            (Some high, Some low) -> 
-              if high.constant < low.constant then begin
-                add_event(CONTRADICTION (high,negate_eq low));
-                raise UNSOLVABLE
-              end
-          | _ -> () end;
-         Hashtbl.remove table ne;
-         Hashtbl.add table ne final
-       with Not_found ->
-         Hashtbl.add table ne 
-           (if kind = NORMAL then (Some nx,None) else (None,Some nx)))
-    system;
-  let accu_eq = ref [] in
-  let accu_ineq = ref [] in
-  Hashtbl.iter
-    (fun p0 p1 -> match (p0,p1) with 
-       | (e, (Some x, Some y)) when x.constant = y.constant -> 
-           let id=new_eq_id () in
-           add_event (MERGE_EQ(id,x,y.id));
-           push {id=id; kind=EQUA; body=x.body; constant=x.constant} accu_eq
-       | (e, (optnorm,optinvert)) ->
-           begin match optnorm with 
-               Some x -> push x accu_ineq | _ -> () end;
-           begin match optinvert with 
-               Some x -> push (negate_eq x) accu_ineq | _ -> () end)
-    table;
-  !accu_eq,!accu_ineq
-
-exception SOLVED_SYSTEM
-
-let select_variable system =
-  let table = Hashtbl.create 7 in
-  let push v c= 
-    try let r = Hashtbl.find table v in r := max !r (abs c)
-    with Not_found -> Hashtbl.add table v (ref (abs c)) in
-  List.iter (fun {body=l} -> List.iter (fun f -> push f.v f.c) l) system;
-  let vmin,cmin = ref (-1), ref 0 in
-  let var_cpt = ref 0 in
-  Hashtbl.iter
-    (fun v ({contents =  c}) ->
-       incr var_cpt;
-       if c < !cmin or !vmin = (-1) then begin vmin := v; cmin := c end)
-    table;
-  if !var_cpt < 1 then raise SOLVED_SYSTEM;
-  !vmin
-
-let classify v system =
-  List.fold_left 
-    (fun (not_occ,below,over) eq ->
-       try let f,eq' = chop_var v eq.body in
-       if f.c >= 0 then (not_occ,((f.c,eq) :: below),over)
-       else (not_occ,below,((-f.c,eq) :: over))
-       with CHOPVAR -> (eq::not_occ,below,over))
-    ([],[],[]) system
-
-let product new_eq_id dark_shadow low high =
-  List.fold_left
-    (fun accu (a,eq1) ->
-       List.fold_left
-         (fun accu (b,eq2) ->
-            let eq = 
-              sum_afine new_eq_id (map_eq_afine (fun c -> c * b) eq1)
-                (map_eq_afine (fun c -> c * a) eq2) in
-            add_event(SUM(eq.id,(b,eq1),(a,eq2)));
-            match normalize eq with
-	      | [eq] ->
-                  let final_eq =
-                    if dark_shadow then 
-                      let delta = (a - 1) * (b - 1) in
-                      add_event(WEAKEN(eq.id,delta));
-                      {id = eq.id; kind=INEQ; body = eq.body; 
-                       constant = eq.constant - delta} 
-                    else eq
-                  in final_eq :: accu
-              | (e::_) -> failwith "Product dardk"
-              | [] -> accu)
-         accu high)
-    [] low
-
-let fourier_motzkin (_,new_eq_id,print_var) dark_shadow system =
-  let v = select_variable system in
-  let (ineq_out, ineq_low,ineq_high) = classify v system in
-  let expanded = ineq_out @ product new_eq_id dark_shadow ineq_low ineq_high in
-  if !debug then display_system print_var expanded; expanded
-
-let simplify ((new_eq_id,new_var_id,print_var) as new_ids) dark_shadow system =
-  if List.exists (fun e -> e.kind = DISE) system then 
-    failwith "disequation in simplify";
-  clear_history ();
-  List.iter (fun e -> add_event (HYP e)) system;
-  let system = flat_map normalize system in
-  let eqs,ineqs = filter (fun e -> e.kind=EQUA) system in
-  let simp_eq,simp_ineq = redundancy_elimination new_eq_id ineqs in
-  let system = (eqs @ simp_eq,simp_ineq) in
-  let rec loop1a system =
-    let sys_ineq = banerjee new_ids system in 
-    loop1b sys_ineq 
-  and loop1b sys_ineq =
-    let simp_eq,simp_ineq = redundancy_elimination new_eq_id sys_ineq in
-    if simp_eq = [] then simp_ineq else loop1a (simp_eq,simp_ineq) 
-  in
-  let rec loop2 system =
-    try
-      let expanded = fourier_motzkin new_ids dark_shadow system in
-      loop2 (loop1b expanded)
-    with SOLVED_SYSTEM ->
-      if !debug then display_system print_var system; system 
-  in
-  loop2 (loop1a system)
-
-let rec depend relie_on accu = function
-  | act :: l -> 
-      begin match act with
-	| DIVIDE_AND_APPROX (e,_,_,_) ->
-            if List.mem e.id relie_on then depend relie_on (act::accu) l
-            else depend relie_on accu l
-	| EXACT_DIVIDE (e,_) ->
-            if List.mem e.id relie_on then depend relie_on (act::accu) l
-            else depend relie_on accu l
-	| WEAKEN (e,_) ->
-            if List.mem e relie_on then depend relie_on (act::accu) l
-            else depend relie_on accu l
-	| SUM (e,(_,e1),(_,e2)) -> 
-            if List.mem e relie_on then 
-	      depend (e1.id::e2.id::relie_on) (act::accu) l
-            else 
-	      depend relie_on accu l
-	| STATE {st_new_eq=e} ->
-            if List.mem e.id relie_on then depend relie_on (act::accu) l
-            else depend relie_on accu l
-	| HYP e ->   
-            if List.mem e.id relie_on then depend relie_on (act::accu) l
-            else depend relie_on accu l
-	| FORGET_C _ -> depend relie_on accu l
-	| FORGET _ -> depend relie_on accu l
-	| FORGET_I _ -> depend relie_on accu l
-	| MERGE_EQ (e,e1,e2) ->
-            if List.mem e relie_on then 
-	      depend (e1.id::e2::relie_on) (act::accu) l
-            else 
-	      depend relie_on accu l
-	| NOT_EXACT_DIVIDE (e,_) -> depend (e.id::relie_on) (act::accu) l
-	| CONTRADICTION (e1,e2) -> 
-	    depend (e1.id::e2.id::relie_on) (act::accu) l
-	| CONSTANT_NOT_NUL (e,_) -> depend (e::relie_on) (act::accu) l
-	| CONSTANT_NEG (e,_) -> depend (e::relie_on) (act::accu) l
-	| CONSTANT_NUL e -> depend (e::relie_on) (act::accu) l
-	| NEGATE_CONTRADICT (e1,e2,_) -> 
-            depend (e1.id::e2.id::relie_on) (act::accu) l
-	| SPLIT_INEQ _ -> failwith "depend"
-      end
-  | [] -> relie_on, accu
-
-(*
-let depend relie_on accu trace = 
-  Printf.printf "Longueur de la trace initiale : %d\n" 
-    (trace_length trace + trace_length accu);
-  let rel',trace' = depend relie_on accu trace in
-  Printf.printf "Longueur de la trace simplifiée : %d\n" (trace_length trace');
-  rel',trace'
-*)
-
-let solve (new_eq_id,new_eq_var,print_var) system =
-  try let _ = simplify new_eq_id false system in failwith "no contradiction"
-  with UNSOLVABLE -> display_action print_var (snd (depend [] [] (history ())))
-      
-let negation (eqs,ineqs) =
-  let diseq,_ = filter (fun e -> e.kind = DISE) ineqs in
-  let normal = function
-    | ({body=f::_} as e) when f.c < 0 ->  negate_eq e, INVERTED
-    | e -> e,NORMAL in
-  let table = Hashtbl.create 7 in
-  List.iter (fun e -> 
-               let {body=ne;constant=c} ,kind = normal e in
-               Hashtbl.add table (ne,c) (kind,e)) diseq;
-  List.iter (fun e ->
-               if e.kind <> EQUA then pp 9999;
-               let {body=ne;constant=c},kind = normal e in
-               try 
-		 let (kind',e') = Hashtbl.find table (ne,c) in
-		 add_event (NEGATE_CONTRADICT (e,e',kind=kind'));
-		 raise UNSOLVABLE
-               with Not_found -> ()) eqs
-
-exception FULL_SOLUTION of action list * int list
-
-let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system =
-  clear_history ();
-  List.iter (fun e -> add_event (HYP e)) system;
-  (* Initial simplification phase *)
-  let rec loop1a system =
-    negation system;
-    let sys_ineq = banerjee new_ids system in 
-    loop1b sys_ineq 
-  and loop1b sys_ineq =
-    let dise,ine = filter (fun e -> e.kind = DISE) sys_ineq in
-    let simp_eq,simp_ineq = redundancy_elimination new_eq_id ine in
-    if simp_eq = [] then dise @ simp_ineq
-    else loop1a (simp_eq,dise @ simp_ineq) 
-  in
-  let rec loop2 system =
-    try
-      let expanded = fourier_motzkin new_ids false system in
-      loop2 (loop1b expanded)
-    with SOLVED_SYSTEM -> if !debug then display_system print_var system; system 
-  in
-  let rec explode_diseq = function 
-    | (de::diseq,ineqs,expl_map) ->
-	let id1 = new_eq_id () 
-	and id2 = new_eq_id () in
-	let e1 = 
-	  {id = id1; kind=INEQ; body = de.body; constant = de.constant - 1} in
-	let e2 = 
-	  {id = id2; kind=INEQ; body = map_eq_linear (fun x -> -x) de.body; 
-           constant = - de.constant - 1} in
-	let new_sys =
-          List.map (fun (what,sys) -> ((de.id,id1,true)::what, e1::sys)) 
-	    ineqs @ 
-          List.map (fun (what,sys) -> ((de.id,id2,false)::what,e2::sys)) 
-	    ineqs 
-	in
-	explode_diseq (diseq,new_sys,(de.id,(de,id1,id2))::expl_map)
-    | ([],ineqs,expl_map) -> ineqs,expl_map 
-  in
-  try 
-    let system = flat_map normalize system in
-    let eqs,ineqs = filter (fun e -> e.kind=EQUA) system in
-    let dise,ine = filter (fun e -> e.kind = DISE) ineqs in
-    let simp_eq,simp_ineq = redundancy_elimination new_eq_id ine in
-    let system = (eqs @ simp_eq,simp_ineq @ dise) in
-    let system' = loop1a system in
-    let diseq,ineq = filter (fun e -> e.kind = DISE) system' in
-    let first_segment = history () in
-    let sys_exploded,explode_map = explode_diseq (diseq,[[],ineq],[]) in
-    let all_solutions =
-      List.map
-        (fun (decomp,sys) -> 
-           clear_history ();
-           try let _ = loop2 sys in raise NO_CONTRADICTION
-           with UNSOLVABLE -> 
-             let relie_on,path = depend [] [] (history ()) in
-             let dc,_ = filter (fun (_,id,_) -> List.mem id relie_on) decomp in
-             let red = List.map (fun (x,_,_) -> x) dc in
-             (red,relie_on,decomp,path))
-        sys_exploded 
-    in
-    let max_count sys = 
-      let tbl = Hashtbl.create 7 in
-      let augment x = 
-        try incr (Hashtbl.find tbl x) 
-	with Not_found -> Hashtbl.add tbl x (ref 1) in
-      let eq = ref (-1) and c = ref 0 in
-      List.iter (function 
-		   | ([],r_on,_,path) -> raise (FULL_SOLUTION (path,r_on))
-                   | (l,_,_,_) -> List.iter augment l) sys;
-      Hashtbl.iter (fun x v -> if !v > !c then begin eq := x; c := !v end) tbl;
-      !eq 
-    in
-    let rec solve systems = 
-      try 
-	let id = max_count systems in 
-        let rec sign = function 
-	  | ((id',_,b)::l) -> if id=id' then b else sign l 
-          | [] -> failwith "solve" in
-        let s1,s2 = filter (fun (_,_,decomp,_) -> sign decomp) systems in
-        let s1' = 
-	  List.map (fun (dep,ro,dc,pa) -> (Util.list_except id dep,ro,dc,pa)) s1 in
-        let s2' = 
-	  List.map (fun (dep,ro,dc,pa) -> (Util.list_except id dep,ro,dc,pa)) s2 in
-        let (r1,relie1) = solve s1' 
-	and (r2,relie2) = solve s2' in
-	let (eq,id1,id2) = List.assoc id explode_map in
-	[SPLIT_INEQ(eq,(id1,r1),(id2, r2))], eq.id :: Util.list_union relie1 relie2
-      with FULL_SOLUTION (x0,x1) -> (x0,x1) 
-    in
-    let act,relie_on = solve all_solutions in
-    snd(depend relie_on act first_segment)
-  with UNSOLVABLE -> snd (depend [] [] (history ()))
diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml
index ef68c5873e..15d8c9beef 100644
--- a/contrib/romega/refl_omega.ml
+++ b/contrib/romega/refl_omega.ml
@@ -139,7 +139,7 @@ and oequation = {
     e_depends: direction  list;		(* liste des points de disjonction dont 
 					   dépend l'accès à l'équation avec la 
 					   direction (branche) pour y accéder *)
-    e_omega: Omega2.afine		(* la fonction normalisée *)
+    e_omega: Omega.afine		(* la fonction normalisée *)
   } 
 
 (* \subsection{Proof context} 
@@ -172,7 +172,7 @@ type environment = {
 type solution = {
   s_index : int;
   s_equa_deps : int list;
-  s_trace : Omega2.action list }
+  s_trace : Omega.action list }
 
 (* Arbre de solution résolvant complètement un ensemble de systèmes *)
 type solution_tree = 
@@ -281,7 +281,7 @@ let get_prop v env = try List.nth v env with _ -> failwith "get_prop"
 (* \subsection{Gestion du nommage des équations} *)
 (* Ajout d'une equation dans l'environnement de reification *)
 let add_equation env e =
-  let id = e.e_omega.Omega2.id in
+  let id = e.e_omega.Omega.id in
   try let _ = Hashtbl.find env.equations id in ()
   with Not_found -> Hashtbl.add env.equations id e
 
@@ -331,12 +331,12 @@ let rec weight env = function
 let omega_of_oformula env kind = 
   let rec loop accu = function
     | Oplus(Omult(v,Oint n),r) -> 
-	loop ({Omega2.v=intern_omega env v; Omega2.c=n} :: accu) r
+	loop ({Omega.v=intern_omega env v; Omega.c=n} :: accu) r
     | Oint n ->
 	let id = new_omega_id () in
 	(*i tag_equation name id; i*)
-	{Omega2.kind = kind; Omega2.body = List.rev accu; 
-	 Omega2.constant = n; Omega2.id = id}
+	{Omega.kind = kind; Omega.body = List.rev accu; 
+	 Omega.constant = n; Omega.id = id}
     | t -> print_string "CO"; oprint stdout t; failwith "compile_equation" in
   loop []
 
@@ -351,10 +351,10 @@ let reified_of_atom env i =
 
 let rec oformula_of_omega env af = 
   let rec loop = function
-    | ({Omega2.v=v; Omega2.c=n}::r) ->
+    | ({Omega.v=v; Omega.c=n}::r) ->
 	Oplus(Omult(unintern_omega env v,Oint n),loop r)
-    | [] -> Oint af.Omega2.constant in
-  loop af.Omega2.body
+    | [] -> Oint af.Omega.constant in
+  loop af.Omega.body
 
 let app f v = mkApp(Lazy.force f,v)
 
@@ -429,7 +429,7 @@ let reified_of_proposition env f =
 let reified_of_omega env body constant = 
   let coeff_constant = 
     app coq_t_int [| mk_Z constant |] in
-  let mk_coeff {Omega2.c=c; Omega2.v=v} t =
+  let mk_coeff {Omega.c=c; Omega.v=v} t =
     let coef = 
       app coq_t_mult 
 	[| reified_of_formula env (unintern_omega env v); 
@@ -441,7 +441,7 @@ let reified_of_omega env body c  =
   begin try 
     reified_of_omega env body c 
   with e -> 
-    Omega2.display_eq display_omega_id (body,c); raise e 
+    Omega.display_eq display_omega_id (body,c); raise e 
   end
 
 (* \section{Opérations sur les équations}
@@ -511,8 +511,8 @@ let rec norm l = (List.length l)
 (* \subsubsection{Version avec coefficients} *)
 let rec shuffle_path k1 e1 k2 e2 =
   let rec loop = function
-      (({Omega2.c=c1;Omega2.v=v1}::l1) as l1'),
-      (({Omega2.c=c2;Omega2.v=v2}::l2) as l2') ->
+      (({Omega.c=c1;Omega.v=v1}::l1) as l1'),
+      (({Omega.c=c2;Omega.v=v2}::l2) as l2') ->
 	if v1 = v2 then
           if k1*c1 + k2 * c2 = 0 then (
             Lazy.force coq_f_cancel :: loop (l1,l2))
@@ -522,9 +522,9 @@ let rec shuffle_path k1 e1 k2 e2 =
 	  Lazy.force coq_f_left :: loop(l1,l2'))
 	else (
 	  Lazy.force coq_f_right :: loop(l1',l2))
-    | ({Omega2.c=c1;Omega2.v=v1}::l1), [] -> 
+    | ({Omega.c=c1;Omega.v=v1}::l1), [] -> 
 	  Lazy.force coq_f_left :: loop(l1,[])
-    | [],({Omega2.c=c2;Omega2.v=v2}::l2) -> 
+    | [],({Omega.c=c2;Omega.v=v2}::l2) -> 
 	  Lazy.force coq_f_right :: loop([],l2)
     | [],[] -> flush stdout; [] in
   mk_shuffle_list (loop (e1,e2))
@@ -681,16 +681,16 @@ let normalize_equation env (negated,depends,origin,path) (oper,t1,t2) =
       e_origin = { o_hyp = origin; o_path = List.rev path };
       e_trace = trace; e_omega = equa } in
   try match (if negated then (negate_oper oper) else oper) with
-    | Eq  -> mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oopp o2)) Omega2.EQUA
-    | Neq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oopp o2)) Omega2.DISE
-    | Leq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o2,Oopp o1)) Omega2.INEQ
-    | Geq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oopp o2)) Omega2.INEQ
+    | Eq  -> mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oopp o2)) Omega.EQUA
+    | Neq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oopp o2)) Omega.DISE
+    | Leq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o2,Oopp o1)) Omega.INEQ
+    | Geq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oopp o2)) Omega.INEQ
     | Lt  ->
         mk_step t1 t2 (fun o1 o2 -> Oplus (Oplus(o2,Oint (-1)),Oopp o1))
-	  Omega2.INEQ
+	  Omega.INEQ
     | Gt ->
         mk_step t1 t2 (fun o1 o2 -> Oplus (Oplus(o1,Oint (-1)),Oopp o2)) 
-	  Omega2.INEQ
+	  Omega.INEQ
   with e when Logic.catchable_exception e -> raise e
 
 (* \section{Compilation des hypothèses} *)
@@ -860,10 +860,10 @@ let display_depend = function
 let display_systems syst_list = 
   let display_omega om_e = 
     Printf.printf "%d : %a %s 0\n"
-      om_e.Omega2.id
-      (fun _ -> Omega2.display_eq display_omega_id) 
-      (om_e.Omega2.body, om_e.Omega2.constant)
-      (Omega2.operator_of_eq om_e.Omega2.kind) in
+      om_e.Omega.id
+      (fun _ -> Omega.display_eq display_omega_id) 
+      (om_e.Omega.body, om_e.Omega.constant)
+      (Omega.operator_of_eq om_e.Omega.kind) in
 
   let display_equation oformula_eq = 
     pprint stdout (Pequa (Lazy.force coq_c_nop,oformula_eq)); print_newline ();
@@ -889,8 +889,8 @@ let display_systems syst_list =
 let rec hyps_used_in_trace = function
   | act :: l -> 
       begin match act with
-	| Omega2.HYP e -> e.Omega2.id :: hyps_used_in_trace l
-	| Omega2.SPLIT_INEQ (_,(_,act1),(_,act2)) -> 
+	| Omega.HYP e -> e.Omega.id :: hyps_used_in_trace l
+	| Omega.SPLIT_INEQ (_,(_,act1),(_,act2)) -> 
 	    hyps_used_in_trace act1 @ hyps_used_in_trace act2
 	| _ -> hyps_used_in_trace l
       end
@@ -903,11 +903,11 @@ let rec hyps_used_in_trace = function
 let rec variable_stated_in_trace = function
   | act :: l -> 
       begin match act with
-	| Omega2.STATE action ->
+	| Omega.STATE action ->
 	    (*i nlle_equa: afine, def: afine, eq_orig: afine, i*)
             (*i coef: int, var:int                            i*)
 	    action :: variable_stated_in_trace l
-	| Omega2.SPLIT_INEQ (_,(_,act1),(_,act2)) -> 
+	| Omega.SPLIT_INEQ (_,(_,act1),(_,act2)) -> 
 	    variable_stated_in_trace act1 @ variable_stated_in_trace act2
 	| _ -> variable_stated_in_trace l
       end
@@ -922,10 +922,10 @@ let add_stated_equations env tree =
   (* Il faut trier les variables par ordre d'introduction pour ne pas risquer
      de définir dans le mauvais ordre *)
   let stated_equations = 
-    List.sort (fun x y -> x.Omega2.st_var - y.Omega2.st_var) (loop tree) in
+    List.sort (fun x y -> x.Omega.st_var - y.Omega.st_var) (loop tree) in
   let add_env st = 
     (* On retransforme la définition de v en formule reifiée *)
-    let v_def = oformula_of_omega env st.Omega2.st_def in
+    let v_def = oformula_of_omega env st.Omega.st_def in
     (* Notez que si l'ordre de création des variables n'est pas respecté, 
      * ca va planter *)
     let coq_v = coq_of_formula env v_def in
@@ -936,8 +936,8 @@ let add_stated_equations env tree =
      * l'environnement pour le faire correctement *)
     let term_to_reify = (v_def,Oatom v) in
     (* enregistre le lien entre la variable omega et la variable Coq *)
-    intern_omega_force env (Oatom v) st.Omega2.st_var; 
-    (v, term_to_generalize,term_to_reify,st.Omega2.st_def.Omega2.id) in
+    intern_omega_force env (Oatom v) st.Omega.st_var; 
+    (v, term_to_generalize,term_to_reify,st.Omega.st_def.Omega.id) in
  List.map add_env stated_equations
 
 (* Calcule la liste des éclatements à réaliser sur les hypothèses 
@@ -982,7 +982,7 @@ let really_useful_prop l_equa c =
   let rec loop c = 
     match c with 
       Pequa(_,e) ->
-	if List.mem e.e_omega.Omega2.id l_equa then Some c else None
+	if List.mem e.e_omega.Omega.id l_equa then Some c else None
     | Ptrue -> None
     | Pfalse -> None
     | Pnot t1 -> 
@@ -1062,59 +1062,59 @@ let get_hyp env_hyp i =
 let replay_history env env_hyp =
   let rec loop env_hyp t =
     match t with
-      | Omega2.CONTRADICTION (e1,e2) :: l -> 
-	  let trace = mk_nat (List.length e1.Omega2.body) in
+      | Omega.CONTRADICTION (e1,e2) :: l -> 
+	  let trace = mk_nat (List.length e1.Omega.body) in
 	  mkApp (Lazy.force coq_s_contradiction,
-		 [| trace ; mk_nat (get_hyp env_hyp e1.Omega2.id); 
-		    mk_nat (get_hyp env_hyp e2.Omega2.id) |])
-      | Omega2.DIVIDE_AND_APPROX (e1,e2,k,d) :: l ->
+		 [| trace ; mk_nat (get_hyp env_hyp e1.Omega.id); 
+		    mk_nat (get_hyp env_hyp e2.Omega.id) |])
+      | Omega.DIVIDE_AND_APPROX (e1,e2,k,d) :: l ->
 	  mkApp (Lazy.force coq_s_div_approx,
 		 [| mk_Z k; mk_Z d; 
-		    reified_of_omega env e2.Omega2.body e2.Omega2.constant;
-		    mk_nat (List.length e2.Omega2.body); 
-		    loop env_hyp l; mk_nat (get_hyp env_hyp e1.Omega2.id) |])
-      | Omega2.NOT_EXACT_DIVIDE (e1,k) :: l ->
-	  let e2_constant = Omega2.floor_div e1.Omega2.constant k in
-	  let d = e1.Omega2.constant - e2_constant * k in
-	  let e2_body = Omega2.map_eq_linear (fun c -> c / k) e1.Omega2.body in
+		    reified_of_omega env e2.Omega.body e2.Omega.constant;
+		    mk_nat (List.length e2.Omega.body); 
+		    loop env_hyp l; mk_nat (get_hyp env_hyp e1.Omega.id) |])
+      | Omega.NOT_EXACT_DIVIDE (e1,k) :: l ->
+	  let e2_constant = Omega.floor_div e1.Omega.constant k in
+	  let d = e1.Omega.constant - e2_constant * k in
+	  let e2_body = Omega.map_eq_linear (fun c -> c / k) e1.Omega.body in
           mkApp (Lazy.force coq_s_not_exact_divide,
 		 [|mk_Z k; mk_Z d; 
 		   reified_of_omega env e2_body e2_constant; 
 		   mk_nat (List.length e2_body); 
-		   mk_nat (get_hyp env_hyp e1.Omega2.id)|])
-      | Omega2.EXACT_DIVIDE (e1,k) :: l ->
+		   mk_nat (get_hyp env_hyp e1.Omega.id)|])
+      | Omega.EXACT_DIVIDE (e1,k) :: l ->
 	  let e2_body =  
-	    Omega2.map_eq_linear (fun c -> c / k) e1.Omega2.body in
-	  let e2_constant = Omega2.floor_div e1.Omega2.constant k in
+	    Omega.map_eq_linear (fun c -> c / k) e1.Omega.body in
+	  let e2_constant = Omega.floor_div e1.Omega.constant k in
           mkApp (Lazy.force coq_s_exact_divide,
 		 [|mk_Z k; 
 		   reified_of_omega env e2_body e2_constant; 
 		   mk_nat (List.length e2_body);
-		   loop env_hyp l; mk_nat (get_hyp env_hyp e1.Omega2.id)|])
-      | (Omega2.MERGE_EQ(e3,e1,e2)) :: l ->
-	  let n1 = get_hyp env_hyp e1.Omega2.id and n2 = get_hyp env_hyp e2 in
+		   loop env_hyp l; mk_nat (get_hyp env_hyp e1.Omega.id)|])
+      | (Omega.MERGE_EQ(e3,e1,e2)) :: l ->
+	  let n1 = get_hyp env_hyp e1.Omega.id and n2 = get_hyp env_hyp e2 in
           mkApp (Lazy.force coq_s_merge_eq,
-		 [| mk_nat (List.length e1.Omega2.body);
+		 [| mk_nat (List.length e1.Omega.body);
 		    mk_nat n1; mk_nat n2;
 		    loop (CCEqua e3:: env_hyp) l |])
-      | Omega2.SUM(e3,(k1,e1),(k2,e2)) :: l ->
-	  let n1 = get_hyp env_hyp e1.Omega2.id 
-	  and n2 = get_hyp env_hyp e2.Omega2.id in
-	  let trace = shuffle_path k1 e1.Omega2.body k2 e2.Omega2.body in
+      | Omega.SUM(e3,(k1,e1),(k2,e2)) :: l ->
+	  let n1 = get_hyp env_hyp e1.Omega.id 
+	  and n2 = get_hyp env_hyp e2.Omega.id in
+	  let trace = shuffle_path k1 e1.Omega.body k2 e2.Omega.body in
           mkApp (Lazy.force coq_s_sum,
 		 [| mk_Z k1; mk_nat n1; mk_Z k2;
 		    mk_nat n2; trace; (loop (CCEqua e3 :: env_hyp) l) |])
-      | Omega2.CONSTANT_NOT_NUL(e,k) :: l -> 
+      | Omega.CONSTANT_NOT_NUL(e,k) :: l -> 
           mkApp (Lazy.force coq_s_constant_not_nul,
 		 [|  mk_nat (get_hyp env_hyp e) |])
-      | Omega2.CONSTANT_NEG(e,k) :: l ->
+      | Omega.CONSTANT_NEG(e,k) :: l ->
           mkApp (Lazy.force coq_s_constant_neg,
 		 [|  mk_nat (get_hyp env_hyp e) |])
-      | Omega2.STATE {Omega2.st_new_eq=new_eq; Omega2.st_def =def; 
-		      Omega2.st_orig=orig; Omega2.st_coef=m;
-                      Omega2.st_var=sigma } :: l ->
-	  let n1 = get_hyp env_hyp orig.Omega2.id 
-	  and n2 = get_hyp env_hyp def.Omega2.id in
+      | Omega.STATE {Omega.st_new_eq=new_eq; Omega.st_def =def; 
+		      Omega.st_orig=orig; Omega.st_coef=m;
+                      Omega.st_var=sigma } :: l ->
+	  let n1 = get_hyp env_hyp orig.Omega.id 
+	  and n2 = get_hyp env_hyp def.Omega.id in
 	  let v = unintern_omega env sigma in
 	  let o_def = oformula_of_omega env def in
 	  let o_orig = oformula_of_omega env orig in
@@ -1123,24 +1123,24 @@ let replay_history env env_hyp =
           let trace,_ = normalize_linear_term env body in
 	  mkApp (Lazy.force coq_s_state,
 		 [| mk_Z m; trace; mk_nat n1; mk_nat n2; 
-		    loop (CCEqua new_eq.Omega2.id :: env_hyp) l |])
-      |	Omega2.HYP _ :: l -> loop env_hyp l
-      |	Omega2.CONSTANT_NUL e :: l ->
+		    loop (CCEqua new_eq.Omega.id :: env_hyp) l |])
+      |	Omega.HYP _ :: l -> loop env_hyp l
+      |	Omega.CONSTANT_NUL e :: l ->
 	  mkApp (Lazy.force coq_s_constant_nul, 
 		 [|  mk_nat (get_hyp env_hyp e) |])
-      |	Omega2.NEGATE_CONTRADICT(e1,e2,b) :: l ->
+      |	Omega.NEGATE_CONTRADICT(e1,e2,b) :: l ->
 	  mkApp (Lazy.force coq_s_negate_contradict, 
-		 [|  mk_nat (get_hyp env_hyp e1.Omega2.id);
-		     mk_nat (get_hyp env_hyp e2.Omega2.id) |])
-      | Omega2.SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: l ->
-	  let i =  get_hyp env_hyp e.Omega2.id in
+		 [|  mk_nat (get_hyp env_hyp e1.Omega.id);
+		     mk_nat (get_hyp env_hyp e2.Omega.id) |])
+      | Omega.SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: l ->
+	  let i =  get_hyp env_hyp e.Omega.id in
 	  let r1 = loop (CCEqua e1 :: env_hyp) l1 in
 	  let r2 = loop (CCEqua e2 :: env_hyp) l2 in
 	  mkApp (Lazy.force coq_s_split_ineq, 
-                  [| mk_nat (List.length e.Omega2.body); mk_nat i; r1 ; r2 |])
-      |	(Omega2.FORGET_C _ | Omega2.FORGET _ | Omega2.FORGET_I _) :: l ->
+                  [| mk_nat (List.length e.Omega.body); mk_nat i; r1 ; r2 |])
+      |	(Omega.FORGET_C _ | Omega.FORGET _ | Omega.FORGET_I _) :: l ->
 	  loop env_hyp l
-      | (Omega2.WEAKEN  _ ) :: l -> failwith "not_treated"
+      | (Omega.WEAKEN  _ ) :: l -> failwith "not_treated"
       |	[] -> failwith "no contradiction"
   in loop env_hyp
 
@@ -1171,7 +1171,7 @@ and decompose_tree_hyps trace env ctxt = function
       let full_path = if equation.e_negated then path @ [O_mono] else path in
       let cont = 
 	decompose_tree_hyps trace env 
-	   (CCEqua equation.e_omega.Omega2.id :: ctxt) l in
+	   (CCEqua equation.e_omega.Omega.id :: ctxt) l in
       app coq_e_extract [|mk_nat index;
 			  mk_direction_list full_path;
 			  cont |]
@@ -1190,7 +1190,7 @@ let resolution env full_reified_goal systems_list =
     let index = !num in
     let system = List.map (fun eq -> eq.e_omega) list_eq in
     let trace = 
-      Omega2.simplify_strong 
+      Omega.simplify_strong 
 	((fun () -> new_eq_id env),new_omega_id,display_omega_id) 
 	system in 
     (* calcule les hypotheses utilisées pour la solution *)
@@ -1198,7 +1198,7 @@ let resolution env full_reified_goal systems_list =
     let splits = get_eclatement env vars in
     if !debug then begin
       Printf.printf "SYSTEME %d\n" index;
-      Omega2.display_action display_omega_id trace;
+      Omega.display_action display_omega_id trace;
       print_string "\n  Depend :";
       List.iter (fun i -> Printf.printf " %d" i) vars;
       print_string "\n  Split points :";
@@ -1299,7 +1299,7 @@ let total_reflexive_omega_tactic gl =
     display_systems systems_list
   end;
   resolution env full_reified_goal systems_list gl
-  with Omega2.NO_CONTRADICTION -> Util.error "ROmega can't solve this system"
+  with Omega.NO_CONTRADICTION -> Util.error "ROmega can't solve this system"
 
 
 (*i let tester = Tacmach.hide_atomic_tactic "TestOmega" test_tactic i*)