Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 1783 insertions, 0 deletions

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
new file mode 100644
index 00000000..7a20aeb6
--- /dev/null
+++ b/contrib/omega/coq_omega.ml
@@ -0,0 +1,1783 @@
+(************************************************************************)
+(*  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)                                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* $Id: coq_omega.ml,v 1.59.2.3 2004/07/16 19:30:12 herbelin Exp $ *)
+
+open Util
+open Pp
+open Reduction
+open Proof_type
+open Ast
+open Names
+open Nameops
+open Term
+open Termops
+open Declarations
+open Environ
+open Sign
+open Inductive
+open Tacticals
+open Tacmach
+open Evar_refiner
+open Tactics
+open Clenv
+open Logic
+open Libnames
+open Nametab
+open Omega
+open Contradiction
+
+(* Added by JCF, 09/03/98 *)
+
+let elim_id id gl = simplest_elim (pf_global gl id) gl
+let resolve_id id gl = apply (pf_global gl id) gl
+
+let timing timer_name f arg = f arg
+
+let display_time_flag = ref false
+let display_system_flag = ref false
+let display_action_flag = ref false
+let old_style_flag = ref false
+
+let read f () = !f
+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;
+      optname  = "Omega system time displaying flag";
+      optkey   = SecondaryTable ("Omega","System");
+      optread  = read display_system_flag;
+      optwrite = write display_system_flag }
+
+let _ =
+  declare_bool_option 
+    { optsync  = false;
+      optname  = "Omega action display flag";
+      optkey   = SecondaryTable ("Omega","Action");
+      optread  = read display_action_flag;
+      optwrite = write display_action_flag }
+
+let _ =
+  declare_bool_option 
+    { optsync  = false;
+      optname  = "Omega old style flag";
+      optkey   = SecondaryTable ("Omega","OldStyle");
+      optread  = read old_style_flag;
+      optwrite = write old_style_flag }
+
+
+let all_time        = timing "Omega     "
+let solver_time     = timing "Solver    "
+let exact_time      = timing "Rewrites  "
+let elim_time       = timing "Elim      "
+let simpl_time      = timing "Simpl     "
+let generalize_time = timing "Generalize"
+
+let new_identifier = 
+  let cpt = ref 0 in 
+  (fun () -> let s = "Omega" ^ string_of_int !cpt in incr cpt; id_of_string s)
+
+let new_identifier_state = 
+  let cpt = ref 0 in 
+  (fun () -> let s = make_ident "State" (Some !cpt) in incr cpt; s)
+
+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 mk_then = tclTHENLIST
+
+let exists_tac c = constructor_tac (Some 1) 1 (Rawterm.ImplicitBindings [c])
+
+let generalize_tac t = generalize_time (generalize t)
+let elim t = elim_time (simplest_elim t)
+let exact t = exact_time (Tactics.refine t)
+let unfold s = Tactics.unfold_in_concl [[], Lazy.force s]
+ 
+let rev_assoc k =
+  let rec loop = function
+    | [] -> raise Not_found | (v,k')::_ when k = k' -> v | _ :: l -> loop l 
+  in
+  loop
+
+let tag_hypothesis,tag_of_hyp, hyp_of_tag =
+  let l = ref ([]:(identifier * int) list) in
+  (fun h id -> l := (h,id):: !l),
+  (fun h -> try List.assoc h !l with Not_found -> failwith "tag_hypothesis"),
+  (fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis")
+
+let hide_constr,find_constr,clear_tables,dump_tables =
+  let l = ref ([]:(constr * (identifier * identifier * bool)) list) in
+  (fun h id eg b -> l := (h,(id,eg,b)):: !l),
+  (fun h -> try List.assoc h !l with Not_found -> failwith "find_contr"),
+  (fun () -> l := []),
+  (fun () -> !l)
+
+(* Lazy evaluation is used for Coq constants, because this code
+ is evaluated before the compiled modules are loaded.
+ To use the constant Zplus, one must type "Lazy.force coq_Zplus"
+ This is the right way to access to Coq constants in tactics ML code *)
+
+open Coqlib
+
+let logic_dir = ["Coq";"Logic";"Decidable"]
+let coq_modules =
+  init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules
+    @ [["Coq"; "omega"; "OmegaLemmas"]]
+
+let constant = gen_constant_in_modules "Omega" coq_modules
+
+(* Zarith *)
+let coq_xH = lazy (constant "xH")
+let coq_xO = lazy (constant "xO")
+let coq_xI = lazy (constant "xI")
+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")
+let coq_INFEEIEUR = lazy (constant "INFERIEUR")
+let coq_EGAL = lazy (constant "EGAL")
+let coq_Zplus = lazy (constant "Zplus")
+let coq_Zmult = lazy (constant "Zmult")
+let coq_Zopp = lazy (constant "Zopp")
+let coq_Zminus = lazy (constant "Zminus")
+let coq_Zs = lazy (constant "Zs")
+let coq_Zgt = lazy (constant "Zgt")
+let coq_Zle = lazy (constant "Zle")
+let coq_inject_nat = lazy (constant "inject_nat")
+let coq_inj_plus = lazy (constant "inj_plus")
+let coq_inj_mult = lazy (constant "inj_mult")
+let coq_inj_minus1 = lazy (constant "inj_minus1")
+let coq_inj_minus2 = lazy (constant "inj_minus2")
+let coq_inj_S = lazy (constant "inj_S")
+let coq_inj_le = lazy (constant "inj_le")
+let coq_inj_lt = lazy (constant "inj_lt")
+let coq_inj_ge = lazy (constant "inj_ge")
+let coq_inj_gt = lazy (constant "inj_gt")
+let coq_inj_neq = lazy (constant "inj_neq")
+let coq_inj_eq = lazy (constant "inj_eq")
+let coq_fast_Zplus_assoc_r = lazy (constant "fast_Zplus_assoc_r")
+let coq_fast_Zplus_assoc_l = lazy (constant "fast_Zplus_assoc_l")
+let coq_fast_Zmult_assoc_r = lazy (constant "fast_Zmult_assoc_r")
+let coq_fast_Zplus_permute = lazy (constant "fast_Zplus_permute")
+let coq_fast_Zplus_sym = lazy (constant "fast_Zplus_sym")
+let coq_fast_Zmult_sym = lazy (constant "fast_Zmult_sym")
+let coq_Zmult_le_approx = lazy (constant "Zmult_le_approx")
+let coq_OMEGA1 = lazy (constant "OMEGA1")
+let coq_OMEGA2 = lazy (constant "OMEGA2")
+let coq_OMEGA3 = lazy (constant "OMEGA3")
+let coq_OMEGA4 = lazy (constant "OMEGA4")
+let coq_OMEGA5 = lazy (constant "OMEGA5")
+let coq_OMEGA6 = lazy (constant "OMEGA6")
+let coq_OMEGA7 = lazy (constant "OMEGA7")
+let coq_OMEGA8 = lazy (constant "OMEGA8")
+let coq_OMEGA9 = lazy (constant "OMEGA9")
+let coq_fast_OMEGA10 = lazy (constant "fast_OMEGA10")
+let coq_fast_OMEGA11 = lazy (constant "fast_OMEGA11")
+let coq_fast_OMEGA12 = lazy (constant "fast_OMEGA12")
+let coq_fast_OMEGA13 = lazy (constant "fast_OMEGA13")
+let coq_fast_OMEGA14 = lazy (constant "fast_OMEGA14")
+let coq_fast_OMEGA15 = lazy (constant "fast_OMEGA15")
+let coq_fast_OMEGA16 = lazy (constant "fast_OMEGA16")
+let coq_OMEGA17 = lazy (constant "OMEGA17")
+let coq_OMEGA18 = lazy (constant "OMEGA18")
+let coq_OMEGA19 = lazy (constant "OMEGA19")
+let coq_OMEGA20 = lazy (constant "OMEGA20")
+let coq_fast_Zred_factor0 = lazy (constant "fast_Zred_factor0")
+let coq_fast_Zred_factor1 = lazy (constant "fast_Zred_factor1")
+let coq_fast_Zred_factor2 = lazy (constant "fast_Zred_factor2")
+let coq_fast_Zred_factor3 = lazy (constant "fast_Zred_factor3")
+let coq_fast_Zred_factor4 = lazy (constant "fast_Zred_factor4")
+let coq_fast_Zred_factor5 = lazy (constant "fast_Zred_factor5")
+let coq_fast_Zred_factor6 = lazy (constant "fast_Zred_factor6")
+let coq_fast_Zmult_plus_distr = lazy (constant "fast_Zmult_plus_distr")
+let coq_fast_Zmult_Zopp_left =  lazy (constant "fast_Zmult_Zopp_left")
+let coq_fast_Zopp_Zplus =   lazy (constant "fast_Zopp_Zplus")
+let coq_fast_Zopp_Zmult_r = lazy (constant "fast_Zopp_Zmult_r")
+let coq_fast_Zopp_one =  lazy (constant "fast_Zopp_one")
+let coq_fast_Zopp_Zopp = lazy (constant "fast_Zopp_Zopp")
+let coq_Zegal_left = lazy (constant "Zegal_left")
+let coq_Zne_left = lazy (constant "Zne_left")
+let coq_Zlt_left = lazy (constant "Zlt_left")
+let coq_Zge_left = lazy (constant "Zge_left")
+let coq_Zgt_left = lazy (constant "Zgt_left")
+let coq_Zle_left = lazy (constant "Zle_left")
+let coq_new_var = lazy (constant "new_var")
+let coq_intro_Z = lazy (constant "intro_Z")
+
+let coq_dec_eq = lazy (constant "dec_eq")
+let coq_dec_Zne = lazy (constant "dec_Zne")
+let coq_dec_Zle = lazy (constant "dec_Zle")
+let coq_dec_Zlt = lazy (constant "dec_Zlt")
+let coq_dec_Zgt = lazy (constant "dec_Zgt")
+let coq_dec_Zge = lazy (constant "dec_Zge")
+
+let coq_not_Zeq = lazy (constant "not_Zeq")
+let coq_not_Zle = lazy (constant "not_Zle")
+let coq_not_Zlt = lazy (constant "not_Zlt")
+let coq_not_Zge = lazy (constant "not_Zge")
+let coq_not_Zgt = lazy (constant "not_Zgt")
+let coq_neq = lazy (constant "neq")
+let coq_Zne = lazy (constant "Zne")
+let coq_Zle = lazy (constant "Zle")
+let coq_Zgt = lazy (constant "Zgt")
+let coq_Zge = lazy (constant "Zge")
+let coq_Zlt = lazy (constant "Zlt")
+
+(* Peano/Datatypes *)
+let coq_le = lazy (constant "le")
+let coq_lt = lazy (constant "lt")
+let coq_ge = lazy (constant "ge")
+let coq_gt = lazy (constant "gt")
+let coq_minus = lazy (constant "minus")
+let coq_plus = lazy (constant "plus")
+let coq_mult = lazy (constant "mult")
+let coq_pred = lazy (constant "pred")
+let coq_nat = lazy (constant "nat")
+let coq_S = lazy (constant "S")
+let coq_O = lazy (constant "O")
+
+(* Compare_dec/Peano_dec/Minus *)
+let coq_pred_of_minus = lazy (constant "pred_of_minus")
+let coq_le_gt_dec = lazy (constant "le_gt_dec")
+let coq_dec_eq_nat = lazy (constant "dec_eq_nat")
+let coq_dec_le = lazy (constant "dec_le")
+let coq_dec_lt = lazy (constant "dec_lt")
+let coq_dec_ge = lazy (constant "dec_ge")
+let coq_dec_gt = lazy (constant "dec_gt")
+let coq_not_eq = lazy (constant "not_eq")
+let coq_not_le = lazy (constant "not_le")
+let coq_not_lt = lazy (constant "not_lt")
+let coq_not_ge = lazy (constant "not_ge")
+let coq_not_gt = lazy (constant "not_gt")
+
+(* Logic/Decidable *)
+let coq_eq_ind_r = lazy (constant "eq_ind_r")
+
+let coq_dec_or = lazy (constant "dec_or")
+let coq_dec_and = lazy (constant "dec_and")
+let coq_dec_imp = lazy (constant "dec_imp")
+let coq_dec_not = lazy (constant "dec_not")
+let coq_dec_False = lazy (constant "dec_False")
+let coq_dec_not_not = lazy (constant "dec_not_not")
+let coq_dec_True = lazy (constant "dec_True")
+
+let coq_not_or = lazy (constant "not_or")
+let coq_not_and = lazy (constant "not_and")
+let coq_not_imp = lazy (constant "not_imp")
+let coq_not_not = lazy (constant "not_not")
+let coq_imp_simp = lazy (constant "imp_simp")
+
+(* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *)
+
+(* For unfold *)
+open Closure
+let evaluable_ref_of_constr s c = match kind_of_term (Lazy.force c) with
+  | Const kn when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) ->
+      EvalConstRef kn
+  | _ -> anomaly ("Coq_omega: "^s^" is not an evaluable constant")
+
+let sp_Zs =     lazy (evaluable_ref_of_constr "Zs" coq_Zs)
+let sp_Zminus = lazy (evaluable_ref_of_constr "Zminus" coq_Zminus)
+let sp_Zle = lazy (evaluable_ref_of_constr "Zle" coq_Zle)
+let sp_Zgt = lazy (evaluable_ref_of_constr "Zgt" coq_Zgt)
+let sp_Zge = lazy (evaluable_ref_of_constr "Zge" coq_Zge)
+let sp_Zlt = lazy (evaluable_ref_of_constr "Zlt" coq_Zlt)
+let sp_not = lazy (evaluable_ref_of_constr "not" (lazy (build_coq_not ())))
+
+let mk_var v = mkVar (id_of_string v)
+let mk_plus t1 t2 = mkApp (Lazy.force coq_Zplus, [| t1; t2 |])
+let mk_times t1 t2 = mkApp (Lazy.force coq_Zmult, [| t1; t2 |])
+let mk_minus t1 t2 = mkApp (Lazy.force coq_Zminus, [| t1;t2 |])
+let mk_eq t1 t2 = mkApp (build_coq_eq (), [| Lazy.force coq_Z; t1; t2 |])
+let mk_le t1 t2 = mkApp (Lazy.force coq_Zle, [| t1; t2 |])
+let mk_gt t1 t2 = mkApp (Lazy.force coq_Zgt, [| t1; t2 |])
+let mk_inv t = mkApp (Lazy.force coq_Zopp, [| t |])
+let mk_and t1 t2 =  mkApp (build_coq_and (), [| t1; t2 |])
+let mk_or t1 t2 =  mkApp (build_coq_or (), [| t1; t2 |])
+let mk_not t = mkApp (build_coq_not (), [| t |])
+let mk_eq_rel t1 t2 = mkApp (build_coq_eq (),
+			      [| Lazy.force coq_relation; t1; t2 |])
+let mk_inj t = mkApp (Lazy.force coq_inject_nat, [| t |])
+
+let mk_integer n =
+  let rec loop n = 
+    if n=1 then Lazy.force coq_xH else 
+      mkApp ((if n mod 2 = 0 then Lazy.force coq_xO else Lazy.force coq_xI),
+		[| loop (n/2) |])
+  in
+  if n = 0 then Lazy.force coq_ZERO 
+  else mkApp ((if n > 0 then Lazy.force coq_POS else Lazy.force coq_NEG),
+		 [| loop (abs n) |])
+    
+type omega_constant =
+  | Zplus | Zmult | Zminus | Zs | Zopp
+  | Plus | Mult | Minus | Pred | S | O
+  | POS | NEG | ZERO | Inject_nat
+  | Eq | Neq
+  | Zne | Zle | Zlt | Zge | Zgt
+  | Z | Nat
+  | And | Or | False | True | Not
+  | Le | Lt | Ge | Gt
+  | Other of string
+
+type omega_proposition =
+  | Keq of constr * constr * constr
+  | Kn
+
+type result = 
+  | Kvar of identifier
+  | Kapp of omega_constant * constr list
+  | Kimp of constr * constr
+  | Kufo
+
+let destructurate_prop t =
+  let c, args = decompose_app t in
+  match kind_of_term c, args with
+    | _, [_;_;_] when c = build_coq_eq () -> Kapp (Eq,args)
+    | _, [_;_] when c = Lazy.force coq_neq -> Kapp (Neq,args)
+    | _, [_;_] when c = Lazy.force coq_Zne -> Kapp (Zne,args)
+    | _, [_;_] when c = Lazy.force coq_Zle -> Kapp (Zle,args)
+    | _, [_;_] when c = Lazy.force coq_Zlt -> Kapp (Zlt,args)
+    | _, [_;_] when c = Lazy.force coq_Zge -> Kapp (Zge,args)
+    | _, [_;_] when c = Lazy.force coq_Zgt -> Kapp (Zgt,args)
+    | _, [_;_] when c = build_coq_and () -> Kapp (And,args)
+    | _, [_;_] when c = build_coq_or () -> Kapp (Or,args)
+    | _, [_] when c = build_coq_not () -> Kapp (Not,args)
+    | _, [] when c = build_coq_False () -> Kapp (False,args)
+    | _, [] when c = build_coq_True () -> Kapp (True,args)
+    | _, [_;_] when c = Lazy.force coq_le -> Kapp (Le,args)
+    | _, [_;_] when c = Lazy.force coq_lt -> Kapp (Lt,args)
+    | _, [_;_] when c = Lazy.force coq_ge -> Kapp (Ge,args)
+    | _, [_;_] when c = Lazy.force coq_gt -> Kapp (Gt,args)
+    | Const sp, args ->
+	Kapp (Other (string_of_id (id_of_global (ConstRef sp))),args)
+    | Construct csp , args ->
+	Kapp (Other (string_of_id (id_of_global (ConstructRef csp))), args)
+    | Ind isp, args ->
+	Kapp (Other (string_of_id (id_of_global (IndRef isp))),args)
+    | Var id,[] -> Kvar id
+    | Prod (Anonymous,typ,body), [] -> Kimp(typ,body)
+    | Prod (Name _,_,_),[] -> error "Omega: Not a quantifier-free goal"
+    | _ -> Kufo
+
+let destructurate_type t =
+  let c, args = decompose_app t in
+  match kind_of_term c, args with
+    | _, [] when c = Lazy.force coq_Z -> Kapp (Z,args)
+    | _, [] when c = Lazy.force coq_nat -> Kapp (Nat,args)
+    | _ -> Kufo
+
+let destructurate_term t =
+  let c, args = decompose_app t in
+  match kind_of_term c, args with
+    | _, [_;_] when c = Lazy.force coq_Zplus -> Kapp (Zplus,args)
+    | _, [_;_] when c = Lazy.force coq_Zmult -> Kapp (Zmult,args)
+    | _, [_;_] when c = Lazy.force coq_Zminus -> Kapp (Zminus,args)
+    | _, [_] when c = Lazy.force coq_Zs -> Kapp (Zs,args)
+    | _, [_] when c = Lazy.force coq_Zopp -> Kapp (Zopp,args)
+    | _, [_;_] when c = Lazy.force coq_plus -> Kapp (Plus,args)
+    | _, [_;_] when c = Lazy.force coq_mult -> Kapp (Mult,args)
+    | _, [_;_] when c = Lazy.force coq_minus -> Kapp (Minus,args)
+    | _, [_] when c = Lazy.force coq_pred -> Kapp (Pred,args)
+    | _, [_] when c = Lazy.force coq_S -> Kapp (S,args)
+    | _, [] when c = Lazy.force coq_O -> Kapp (O,args)
+    | _, [_] when c = Lazy.force coq_POS -> Kapp (NEG,args)
+    | _, [_] when c = Lazy.force coq_NEG -> Kapp (POS,args)
+    | _, [] when c = Lazy.force coq_ZERO -> Kapp (ZERO,args)
+    | _, [_] when c = Lazy.force coq_inject_nat -> Kapp (Inject_nat,args)
+    | Var id,[] -> Kvar id
+    | _ -> Kufo
+
+let recognize_number t =
+  let rec loop t =
+    match decompose_app t with
+      | f, [t] when f = Lazy.force coq_xI -> 1 + 2 * loop t
+      | f, [t] when f = Lazy.force coq_xO -> 2 * loop t
+      | f, [] when f = Lazy.force coq_xH -> 1
+      | _ -> failwith "not a number" 
+  in
+  match decompose_app t with 
+    | f, [t] when f = Lazy.force coq_POS -> loop t
+    | f, [t] when f = Lazy.force coq_NEG -> - (loop t)
+    | f, [] when f = Lazy.force coq_ZERO -> 0
+    | _ -> failwith "not a number"
+	  
+type constr_path =
+  | P_APP of int
+  (* Abstraction and product *)
+  | P_BODY 
+  | P_TYPE
+  (* Case *)
+  | P_BRANCH of int
+  | P_ARITY
+  | P_ARG
+
+let context operation path (t : constr) =
+  let rec loop i p0 t = 
+    match (p0,kind_of_term t) with 
+      | (p, Cast (c,t)) -> mkCast (loop i p c,t)
+      | ([], _) -> operation i t
+      | ((P_APP n :: p),  App (f,v)) ->
+(*	  let f,l = get_applist t in   NECESSAIRE ??
+	  let v' = Array.of_list (f::l) in  *)
+	  let v' = Array.copy v in
+	  v'.(n-1) <- loop i p v'.(n-1); mkApp (f, v')
+      | ((P_BRANCH n :: p), Case (ci,q,c,v)) ->
+	  (* avant, y avait mkApp... anyway, BRANCH seems nowhere used *)
+	  let v' = Array.copy v in
+	  v'.(n) <- loop i p v'.(n); (mkCase (ci,q,c,v'))
+      | ((P_ARITY :: p),  App (f,l)) ->
+	  appvect (loop i p f,l)
+      | ((P_ARG :: p),  App (f,v)) ->
+	  let v' = Array.copy v in
+	  v'.(0) <- loop i p v'.(0); mkApp (f,v')
+      | (p, Fix ((_,n as ln),(tys,lna,v))) ->
+	  let l = Array.length v in
+	  let v' = Array.copy v in
+	  v'.(n) <- loop (i+l) p v.(n); (mkFix (ln,(tys,lna,v')))
+      | ((P_BODY :: p), Prod (n,t,c)) ->
+	  (mkProd (n,t,loop (i+1) p c))
+      | ((P_BODY :: p), Lambda (n,t,c)) ->
+	  (mkLambda (n,t,loop (i+1) p c))
+      | ((P_BODY :: p), LetIn (n,b,t,c)) ->
+	  (mkLetIn (n,b,t,loop (i+1) p c))
+      | ((P_TYPE :: p), Prod (n,t,c)) ->
+	  (mkProd (n,loop i p t,c))
+      | ((P_TYPE :: p), Lambda (n,t,c)) ->
+	  (mkLambda (n,loop i p t,c))
+      | ((P_TYPE :: p), LetIn (n,b,t,c)) ->
+	  (mkLetIn (n,b,loop i p t,c))
+      | (p, _) -> 
+	  ppnl (Printer.prterm t);
+	  failwith ("abstract_path " ^ string_of_int(List.length p)) 
+  in
+  loop 1 path t
+
+let occurence path (t : constr) =
+  let rec loop p0 t = match (p0,kind_of_term t) with
+    | (p, Cast (c,t)) -> loop p c
+    | ([], _) -> t
+    | ((P_APP n :: p),  App (f,v)) -> loop p v.(n-1)
+    | ((P_BRANCH n :: p), Case (_,_,_,v)) -> loop p v.(n)
+    | ((P_ARITY :: p),  App (f,_)) -> loop p f
+    | ((P_ARG :: p),  App (f,v)) -> loop p v.(0)
+    | (p, Fix((_,n) ,(_,_,v))) -> loop p v.(n)
+    | ((P_BODY :: p), Prod (n,t,c)) -> loop p c
+    | ((P_BODY :: p), Lambda (n,t,c)) -> loop p c
+    | ((P_BODY :: p), LetIn (n,b,t,c)) -> loop p c
+    | ((P_TYPE :: p), Prod (n,term,c)) -> loop p term
+    | ((P_TYPE :: p), Lambda (n,term,c)) -> loop p term
+    | ((P_TYPE :: p), LetIn (n,b,term,c)) -> loop p term
+    | (p, _) -> 
+	ppnl (Printer.prterm t);
+	failwith ("occurence " ^ string_of_int(List.length p)) 
+  in
+  loop path t
+
+let abstract_path typ path t =
+  let term_occur = ref (mkRel 0) in
+  let abstract = context (fun i t -> term_occur:= t; mkRel i) path t in
+  mkLambda (Name (id_of_string "x"), typ, abstract), !term_occur
+
+let focused_simpl path gl =
+  let newc = context (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in
+  convert_concl_no_check newc gl
+
+let focused_simpl path = simpl_time (focused_simpl path)
+
+type oformula =
+  | Oplus of oformula * oformula
+  | Oinv of  oformula
+  | Otimes of oformula * oformula
+  | Oatom of identifier
+  | Oz of int
+  | Oufo of constr
+
+let rec oprint = function 
+  | Oplus(t1,t2) -> 
+      print_string "("; oprint t1; print_string "+"; 
+      oprint t2; print_string ")"
+  | Oinv t -> print_string "~"; oprint t
+  | Otimes (t1,t2) -> 
+      print_string "("; oprint t1; print_string "*"; 
+      oprint t2; print_string ")"
+  | Oatom s -> print_string (string_of_id s)
+  | Oz i -> print_int i
+  | Oufo f -> print_string "?"
+
+let rec weight = function
+  | Oatom c -> intern_id c
+  | Oz _ -> -1
+  | Oinv c -> weight c
+  | Otimes(c,_) -> weight c
+  | Oplus _ -> failwith "weight"
+  | Oufo _ -> -1
+
+let rec val_of = function
+  | Oatom c -> mkVar c
+  | Oz c -> mk_integer c
+  | Oinv c -> mkApp (Lazy.force coq_Zopp, [| val_of c |])
+  | Otimes (t1,t2) -> mkApp (Lazy.force coq_Zmult, [| val_of t1; val_of t2 |])
+  | Oplus(t1,t2) -> mkApp (Lazy.force coq_Zplus, [| val_of t1; val_of t2 |])
+  | Oufo c -> c
+
+let compile name kind = 
+  let rec loop accu = function
+    | Oplus(Otimes(Oatom v,Oz n),r) -> loop ({v=intern_id v; c=n} :: accu) r
+    | Oz n ->
+	let id = new_id () in
+	tag_hypothesis name id;
+	{kind = kind; body = List.rev accu; constant = n; id = id}
+    | _ -> anomaly "compile_equation" 
+  in
+  loop []
+
+let rec decompile af = 
+  let rec loop = function
+    | ({v=v; c=n}::r) -> Oplus(Otimes(Oatom (unintern_id v),Oz n),loop r) 
+    | [] -> Oz af.constant 
+  in
+  loop af.body
+
+let mkNewMeta () = mkMeta (Clenv.new_meta())
+
+let clever_rewrite_base_poly typ p result theorem gl = 
+  let full = pf_concl gl in
+  let (abstracted,occ) = abstract_path typ (List.rev p) full in
+  let t = 
+    applist
+      (mkLambda
+	 (Name (id_of_string "P"), 
+	  mkArrow typ mkProp,
+          mkLambda
+	    (Name (id_of_string "H"),
+	     applist (mkRel 1,[result]),
+	     mkApp (Lazy.force coq_eq_ind_r, 
+		       [| typ; result; mkRel 2; mkRel 1; occ; theorem |]))),
+       [abstracted]) 
+  in
+  exact (applist(t,[mkNewMeta()])) gl
+
+let clever_rewrite_base p result theorem gl = 
+  clever_rewrite_base_poly (Lazy.force coq_Z) p result theorem gl
+
+let clever_rewrite_base_nat p result theorem gl = 
+  clever_rewrite_base_poly (Lazy.force coq_nat) p result theorem gl
+
+let clever_rewrite_gen p result (t,args) = 
+  let theorem = applist(t, args) in 
+  clever_rewrite_base p result theorem
+
+let clever_rewrite_gen_nat p result (t,args) = 
+  let theorem = applist(t, args) in 
+  clever_rewrite_base_nat p result theorem
+
+let clever_rewrite p vpath t gl = 
+  let full = pf_concl gl in
+  let (abstracted,occ) = abstract_path (Lazy.force coq_Z) (List.rev p) full in
+  let vargs = List.map (fun p -> occurence p occ) vpath in
+  let t' = applist(t, (vargs @ [abstracted])) in
+  exact (applist(t',[mkNewMeta()])) gl
+    
+let rec shuffle p (t1,t2) = 
+  match t1,t2 with
+    | Oplus(l1,r1), Oplus(l2,r2) ->
+	if weight l1 > weight l2 then 
+          let (tac,t') = shuffle (P_APP 2 :: p) (r1,t2) in
+          (clever_rewrite p [[P_APP 1;P_APP 1]; 
+			     [P_APP 1; P_APP 2];[P_APP 2]]
+             (Lazy.force coq_fast_Zplus_assoc_r)
+           :: tac,
+           Oplus(l1,t'))
+	else 
+	  let (tac,t') = shuffle (P_APP 2 :: p) (t1,r2) in
+          (clever_rewrite p [[P_APP 1];[P_APP 2;P_APP 1];[P_APP 2;P_APP 2]]
+             (Lazy.force coq_fast_Zplus_permute)
+           :: tac,
+           Oplus(l2,t'))
+    | Oplus(l1,r1), t2 -> 
+	if weight l1 > weight t2 then
+          let (tac,t') = shuffle (P_APP 2 :: p) (r1,t2) in
+          clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]]
+            (Lazy.force coq_fast_Zplus_assoc_r)
+          :: tac, 
+          Oplus(l1, t')
+	else 
+          [clever_rewrite p [[P_APP 1];[P_APP 2]] 
+	     (Lazy.force coq_fast_Zplus_sym)],
+          Oplus(t2,t1)
+    | t1,Oplus(l2,r2) -> 
+	if weight l2 > weight t1 then
+          let (tac,t') = shuffle (P_APP 2 :: p) (t1,r2) in
+          clever_rewrite p [[P_APP 1];[P_APP 2;P_APP 1];[P_APP 2;P_APP 2]]
+            (Lazy.force coq_fast_Zplus_permute)
+          :: tac,
+          Oplus(l2,t')
+	else [],Oplus(t1,t2)
+    | Oz t1,Oz t2 ->
+	[focused_simpl p], Oz(t1+t2)
+    | t1,t2 ->
+	if weight t1 < weight t2 then
+          [clever_rewrite p [[P_APP 1];[P_APP 2]] 
+	     (Lazy.force coq_fast_Zplus_sym)],
+	  Oplus(t2,t1)
+	else [],Oplus(t1,t2)
+	  
+let rec shuffle_mult p_init k1 e1 k2 e2 =
+  let rec loop p = function
+    | (({c=c1;v=v1}::l1) as l1'),(({c=c2;v=v2}::l2) as l2') ->
+	if v1 = v2 then
+          let tac =
+            clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1; P_APP 1];
+                              [P_APP 1; P_APP 1; P_APP 1; P_APP 2];
+                              [P_APP 2; P_APP 1; P_APP 1; P_APP 2];
+                              [P_APP 1; P_APP 1; P_APP 2];
+                              [P_APP 2; P_APP 1; P_APP 2];
+                              [P_APP 1; P_APP 2];
+                              [P_APP 2; P_APP 2]]
+              (Lazy.force coq_fast_OMEGA10) 
+	  in
+          if k1*c1 + k2 * c2 = 0 then 
+            let tac' = 
+	      clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]]
+                (Lazy.force coq_fast_Zred_factor5) in
+	    tac :: focused_simpl (P_APP 1::P_APP 2:: p) :: tac' :: 
+	    loop p (l1,l2)
+          else tac :: loop (P_APP 2 :: p) (l1,l2)
+	else if v1 > v2 then
+          clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1; P_APP 1];
+                            [P_APP 1; P_APP 1; P_APP 1; P_APP 2];
+                            [P_APP 1; P_APP 1; P_APP 2];
+                            [P_APP 2];
+                            [P_APP 1; P_APP 2]]
+            (Lazy.force coq_fast_OMEGA11) ::
+          loop (P_APP 2 :: p) (l1,l2')
+	else
+          clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1];
+                            [P_APP 2; P_APP 1; P_APP 1; P_APP 2];
+                            [P_APP 1];
+                            [P_APP 2; P_APP 1; P_APP 2];
+                            [P_APP 2; P_APP 2]]
+            (Lazy.force coq_fast_OMEGA12) ::
+          loop (P_APP 2 :: p) (l1',l2)
+    | ({c=c1;v=v1}::l1), [] -> 
+        clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1; P_APP 1];
+                          [P_APP 1; P_APP 1; P_APP 1; P_APP 2];
+                          [P_APP 1; P_APP 1; P_APP 2];
+                          [P_APP 2];
+                          [P_APP 1; P_APP 2]]
+          (Lazy.force coq_fast_OMEGA11) ::
+        loop (P_APP 2 :: p) (l1,[])
+    | [],({c=c2;v=v2}::l2) -> 
+        clever_rewrite p  [[P_APP 2; P_APP 1; P_APP 1; P_APP 1];
+                           [P_APP 2; P_APP 1; P_APP 1; P_APP 2];
+                           [P_APP 1];
+                           [P_APP 2; P_APP 1; P_APP 2];
+                           [P_APP 2; P_APP 2]]
+          (Lazy.force coq_fast_OMEGA12) ::
+        loop (P_APP 2 :: p) ([],l2)
+    | [],[] -> [focused_simpl p_init] 
+  in
+  loop p_init (e1,e2)
+    
+let rec shuffle_mult_right p_init e1 k2 e2 =
+  let rec loop p = function
+    | (({c=c1;v=v1}::l1) as l1'),(({c=c2;v=v2}::l2) as l2') ->
+	if v1 = v2 then
+          let tac =
+            clever_rewrite p
+              [[P_APP 1; P_APP 1; P_APP 1];
+               [P_APP 1; P_APP 1; P_APP 2];
+               [P_APP 2; P_APP 1; P_APP 1; P_APP 2];
+               [P_APP 1; P_APP 2];
+               [P_APP 2; P_APP 1; P_APP 2];
+               [P_APP 2; P_APP 2]]
+              (Lazy.force coq_fast_OMEGA15) 
+	  in
+          if c1 + k2 * c2 = 0 then 
+            let tac' = 
+              clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]]
+                (Lazy.force coq_fast_Zred_factor5) 
+	    in
+            tac :: focused_simpl (P_APP 1::P_APP 2:: p) :: tac' :: 
+            loop p (l1,l2)
+          else tac :: loop (P_APP 2 :: p) (l1,l2)
+	else if v1 > v2 then
+          clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]]
+            (Lazy.force coq_fast_Zplus_assoc_r) ::
+          loop (P_APP 2 :: p) (l1,l2')
+	else
+          clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1];
+                            [P_APP 2; P_APP 1; P_APP 1; P_APP 2];
+                            [P_APP 1];
+                            [P_APP 2; P_APP 1; P_APP 2];
+                            [P_APP 2; P_APP 2]]
+            (Lazy.force coq_fast_OMEGA12) ::
+          loop (P_APP 2 :: p) (l1',l2)
+    | ({c=c1;v=v1}::l1), [] -> 
+        clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]]
+          (Lazy.force coq_fast_Zplus_assoc_r) ::
+        loop (P_APP 2 :: p) (l1,[])
+    | [],({c=c2;v=v2}::l2) -> 
+        clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1];
+                          [P_APP 2; P_APP 1; P_APP 1; P_APP 2];
+                          [P_APP 1];
+                          [P_APP 2; P_APP 1; P_APP 2];
+                          [P_APP 2; P_APP 2]]
+          (Lazy.force coq_fast_OMEGA12) ::
+        loop (P_APP 2 :: p) ([],l2)
+    | [],[] -> [focused_simpl p_init] 
+  in
+  loop p_init (e1,e2)
+
+let rec shuffle_cancel p = function 
+  | [] -> [focused_simpl p]
+  | ({c=c1}::l1) ->
+      let tac = 
+	clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1];[P_APP 1; P_APP 2];
+                          [P_APP 2; P_APP 2]; 
+                          [P_APP 1; P_APP 1; P_APP 2; P_APP 1]]
+          (if c1 > 0 then 
+	     (Lazy.force coq_fast_OMEGA13) 
+	   else 
+	     (Lazy.force coq_fast_OMEGA14)) 
+      in
+      tac :: shuffle_cancel p l1
+	
+let rec scalar p n = function
+  | Oplus(t1,t2) -> 
+      let tac1,t1' = scalar (P_APP 1 :: p) n t1 and 
+        tac2,t2' = scalar (P_APP 2 :: p) n t2 in
+      clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2]]
+        (Lazy.force coq_fast_Zmult_plus_distr) :: 
+      (tac1 @ tac2), Oplus(t1',t2')
+  | Oinv t ->
+      [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] 
+	 (Lazy.force coq_fast_Zmult_Zopp_left);
+       focused_simpl (P_APP 2 :: p)], Otimes(t,Oz(-n))
+  | Otimes(t1,Oz x) -> 
+      [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2]]
+         (Lazy.force coq_fast_Zmult_assoc_r);
+       focused_simpl (P_APP 2 :: p)], 
+      Otimes(t1,Oz (n*x))
+  | Otimes(t1,t2) -> error "Omega: Can't solve a goal with non-linear products"
+  | (Oatom _ as t) -> [], Otimes(t,Oz n)
+  | Oz i -> [focused_simpl p],Oz(n*i)
+  | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zmult, [| mk_integer n; c |]))
+      
+let rec scalar_norm p_init = 
+  let rec loop p = function
+    | [] -> [focused_simpl p_init]
+    | (_::l) -> 
+	clever_rewrite p
+          [[P_APP 1; P_APP 1; P_APP 1];[P_APP 1; P_APP 1; P_APP 2];
+           [P_APP 1; P_APP 2];[P_APP 2]]
+          (Lazy.force coq_fast_OMEGA16) :: loop (P_APP 2 :: p) l 
+  in
+  loop p_init
+
+let rec norm_add p_init =
+  let rec loop p = function
+    | [] -> [focused_simpl p_init]
+    | _:: l -> 
+	clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]]
+          (Lazy.force coq_fast_Zplus_assoc_r) ::
+	loop (P_APP 2 :: p) l 
+  in
+  loop p_init
+
+let rec scalar_norm_add p_init =
+  let rec loop p = function
+    | [] -> [focused_simpl p_init]
+    | _ :: l -> 
+	clever_rewrite p
+          [[P_APP 1; P_APP 1; P_APP 1; P_APP 1];
+           [P_APP 1; P_APP 1; P_APP 1; P_APP 2];
+           [P_APP 1; P_APP 1; P_APP 2]; [P_APP 2]; [P_APP 1; P_APP 2]]
+          (Lazy.force coq_fast_OMEGA11) :: loop (P_APP 2 :: p) l 
+  in
+  loop p_init
+
+let rec negate p = function
+  | Oplus(t1,t2) -> 
+      let tac1,t1' = negate (P_APP 1 :: p) t1 and 
+        tac2,t2' = negate (P_APP 2 :: p) t2 in
+      clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2]]
+        (Lazy.force coq_fast_Zopp_Zplus) :: 
+      (tac1 @ tac2),
+      Oplus(t1',t2')
+  | Oinv t ->
+      [clever_rewrite p [[P_APP 1;P_APP 1]] (Lazy.force coq_fast_Zopp_Zopp)], t
+  | Otimes(t1,Oz x) -> 
+      [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2]]
+         (Lazy.force coq_fast_Zopp_Zmult_r);
+       focused_simpl (P_APP 2 :: p)], Otimes(t1,Oz (-x))
+  | Otimes(t1,t2) -> error "Omega: Can't solve a goal with non-linear products"
+  | (Oatom _ as t) ->
+      let r = Otimes(t,Oz(-1)) in
+      [clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zopp_one)], r
+  | Oz i -> [focused_simpl p],Oz(-i)
+  | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zopp, [| c |]))
+      
+let rec transform p t = 
+  let default () =
+    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 false;
+      [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v
+  in
+  try match destructurate_term t with
+    | Kapp(Zplus,[t1;t2]) ->
+	let tac1,t1' = transform (P_APP 1 :: p) t1 
+	and tac2,t2' = transform (P_APP 2 :: p) t2 in
+	let tac,t' = shuffle p (t1',t2') in
+	tac1 @ tac2 @ tac, t'
+    | Kapp(Zminus,[t1;t2]) ->
+	let tac,t = 
+	  transform p
+	    (mkApp (Lazy.force coq_Zplus,
+		     [| t1; (mkApp (Lazy.force coq_Zopp, [| t2 |])) |])) in
+	unfold sp_Zminus :: tac,t
+    | Kapp(Zs,[t1]) ->
+	let tac,t = transform p (mkApp (Lazy.force coq_Zplus,
+					 [| t1; mk_integer 1 |])) in
+	unfold sp_Zs :: tac,t
+   | Kapp(Zmult,[t1;t2]) ->
+       let tac1,t1' = transform (P_APP 1 :: p) t1 
+       and tac2,t2' = transform (P_APP 2 :: p) t2 in
+       begin match t1',t2' with
+         | (_,Oz n) -> let tac,t' = scalar p n t1' in tac1 @ tac2 @ tac,t'
+         | (Oz n,_) ->
+             let sym = 
+	       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 ()
+       end
+   | Kapp((POS|NEG|ZERO),_) -> 
+       (try ([],Oz(recognize_number t)) with _ -> default ())
+   | 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 ()
+      
+let shrink_pair p f1 f2 =
+  match f1,f2 with
+    | Oatom v,Oatom _ -> 
+	let r = Otimes(Oatom v,Oz 2) in
+	clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zred_factor1), r
+    | Oatom v, Otimes(_,c2) -> 
+	let r = Otimes(Oatom v,Oplus(c2,Oz 1)) in
+	clever_rewrite p [[P_APP 1];[P_APP 2;P_APP 2]] 
+	  (Lazy.force coq_fast_Zred_factor2), r
+    | Otimes (v1,c1),Oatom v -> 
+	let r = Otimes(Oatom v,Oplus(c1,Oz 1)) in
+	clever_rewrite p [[P_APP 2];[P_APP 1;P_APP 2]]
+          (Lazy.force coq_fast_Zred_factor3), r
+    | Otimes (Oatom v,c1),Otimes (v2,c2) ->
+	let r = Otimes(Oatom v,Oplus(c1,c2)) in
+	clever_rewrite p 
+          [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2;P_APP 2]]
+          (Lazy.force coq_fast_Zred_factor4),r
+    | t1,t2 -> 
+	begin 
+	  oprint t1; print_newline (); oprint t2; print_newline (); 
+	  flush Pervasives.stdout; error "shrink.1"
+	end
+
+let reduce_factor p = function
+  | Oatom v ->
+      let r = Otimes(Oatom v,Oz 1) in
+      [clever_rewrite p [[]] (Lazy.force coq_fast_Zred_factor0)],r
+  | Otimes(Oatom v,Oz n) as f -> [],f
+  | Otimes(Oatom v,c) ->
+      let rec compute = function
+        | Oz n -> n
+	| Oplus(t1,t2) -> compute t1 + compute t2 
+	| _ -> error "condense.1" 
+      in
+      [focused_simpl (P_APP 2 :: p)], Otimes(Oatom v,Oz(compute c))
+  | t -> oprint t; error "reduce_factor.1"
+
+let rec condense p = function
+  | Oplus(f1,(Oplus(f2,r) as t)) ->
+      if weight f1 = weight f2 then begin
+	let shrink_tac,t = shrink_pair (P_APP 1 :: p) f1 f2 in
+	let assoc_tac = 
+          clever_rewrite p 
+            [[P_APP 1];[P_APP 2;P_APP 1];[P_APP 2;P_APP 2]]
+            (Lazy.force coq_fast_Zplus_assoc_l) in
+	let tac_list,t' = condense p (Oplus(t,r)) in
+	(assoc_tac :: shrink_tac :: tac_list), t'
+      end else begin
+	let tac,f = reduce_factor (P_APP 1 :: p) f1 in
+	let tac',t' = condense (P_APP 2 :: p) t in 
+	(tac @ tac'), Oplus(f,t') 
+      end
+  | Oplus(f1,Oz n) as t -> 
+      let tac,f1' = reduce_factor (P_APP 1 :: p) f1 in tac,Oplus(f1',Oz n)
+  | Oplus(f1,f2) -> 
+      if weight f1 = weight f2 then begin
+	let tac_shrink,t = shrink_pair p f1 f2 in
+	let tac,t' = condense p t in
+	tac_shrink :: tac,t'
+      end else begin
+	let tac,f = reduce_factor (P_APP 1 :: p) f1 in
+	let tac',t' = condense (P_APP 2 :: p) f2 in 
+	(tac @ tac'),Oplus(f,t') 
+      end
+  | Oz _ as t -> [],t
+  | t -> 
+      let tac,t' = reduce_factor p t in
+      let final = Oplus(t',Oz 0) in
+      let tac' = clever_rewrite p [[]] (Lazy.force coq_fast_Zred_factor6) in
+      tac @ [tac'], final
+
+let rec clear_zero p = function
+  | Oplus(Otimes(Oatom v,Oz 0),r) ->
+      let tac =
+	clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] 
+	  (Lazy.force coq_fast_Zred_factor5) in
+      let tac',t = clear_zero p r in
+      tac :: tac',t
+  | Oplus(f,r) -> 
+      let tac,t = clear_zero (P_APP 2 :: p) r in tac,Oplus(f,t)
+  | t -> [],t
+
+let replay_history tactic_normalisation = 
+  let aux  = id_of_string "auxiliary" in
+  let aux1 = id_of_string "auxiliary_1" in
+  let aux2 = id_of_string "auxiliary_2" in
+  let zero = mk_integer 0 in
+  let rec loop t =
+    match t with
+      | HYP e :: l -> 
+	  begin 
+	    try 
+	      tclTHEN 
+		(List.assoc (hyp_of_tag e.id) tactic_normalisation) 
+		(loop l)
+	    with Not_found -> loop l end
+      | NEGATE_CONTRADICT (e2,e1,b) :: l ->
+	  let eq1 = decompile e1 
+	  and eq2 = decompile e2 in 
+	  let id1 = hyp_of_tag e1.id 
+	  and id2 = hyp_of_tag e2.id in
+	  let k = if b then (-1) else 1 in
+	  let p_initial = [P_APP 1;P_TYPE] in
+	  let tac= shuffle_mult_right p_initial e1.body k e2.body in
+	  tclTHENLIST [
+	    (generalize_tac 
+	      [mkApp (Lazy.force coq_OMEGA17, [| 
+		val_of eq1;
+		val_of eq2;
+		mk_integer k; 
+		mkVar id1; mkVar id2 |])]);
+	    (mk_then tac);
+	    (intros_using [aux]);
+	    (resolve_id aux);
+            reflexivity
+          ]
+      | CONTRADICTION (e1,e2) :: l -> 
+	  let eq1 = decompile e1 
+	  and eq2 = decompile e2 in 
+	  let p_initial = [P_APP 2;P_TYPE] in
+	  let tac = shuffle_cancel p_initial e1.body in
+	  let solve_le =
+            let superieur = Lazy.force coq_SUPERIEUR in
+            let not_sup_sup = mkApp (build_coq_eq (), [| 
+					Lazy.force coq_relation; 
+					Lazy.force coq_SUPERIEUR;
+					Lazy.force coq_SUPERIEUR |])
+	    in
+            tclTHENS 
+	      (tclTHENLIST [
+		(unfold sp_Zle);
+		(simpl_in_concl);
+		intro;
+		(absurd not_sup_sup) ])
+	      [ assumption ; reflexivity ] 
+	  in
+	  let theorem =
+            mkApp (Lazy.force coq_OMEGA2, [| 
+		      val_of eq1; val_of eq2; 
+		      mkVar (hyp_of_tag e1.id);
+		      mkVar (hyp_of_tag e2.id) |])
+	  in
+	  tclTHEN (tclTHEN (generalize_tac [theorem]) (mk_then tac)) (solve_le)
+      | DIVIDE_AND_APPROX (e1,e2,k,d) :: l ->
+	  let id = hyp_of_tag e1.id in
+	  let eq1 = val_of(decompile e1) 
+	  and eq2 = val_of(decompile e2) in
+	  let kk = mk_integer k 
+	  and dd = mk_integer d in
+	  let rhs = mk_plus (mk_times eq2 kk) dd in
+	  let state_eg = mk_eq eq1 rhs in
+	  let tac = scalar_norm_add [P_APP 3] e2.body in
+	  tclTHENS 
+	    (cut state_eg) 
+	    [ tclTHENS
+	        (tclTHENLIST [
+		  (intros_using [aux]);
+		  (generalize_tac 
+		    [mkApp (Lazy.force coq_OMEGA1,
+		      [| eq1; rhs; mkVar aux; mkVar id |])]);
+		  (clear [aux;id]);
+		  (intros_using [id]);
+		  (cut (mk_gt kk dd)) ])
+	        [ tclTHENS 
+		    (cut (mk_gt kk zero)) 
+		    [ tclTHENLIST [
+		        (intros_using [aux1; aux2]);
+		        (generalize_tac 
+			  [mkApp (Lazy.force coq_Zmult_le_approx,
+			    [| kk;eq2;dd;mkVar aux1;mkVar aux2; mkVar id |])]);
+		        (clear [aux1;aux2;id]);
+		        (intros_using [id]);
+		        (loop l) ];
+		      tclTHENLIST [
+			(unfold sp_Zgt);
+			(simpl_in_concl);
+			reflexivity ] ];
+		  tclTHENLIST [ (unfold sp_Zgt); simpl_in_concl; reflexivity ]
+                ];
+	      tclTHEN (mk_then tac) reflexivity ]
+	    
+      | NOT_EXACT_DIVIDE (e1,k) :: l ->
+	  let id = hyp_of_tag e1.id in
+	  let c = floor_div e1.constant k in
+	  let d = e1.constant - c * k in
+	  let e2 =  {id=e1.id; kind=EQUA;constant = c; 
+                     body = map_eq_linear (fun c -> c / k) e1.body } in
+	  let eq1 = val_of(decompile e1) 
+	  and eq2 = val_of(decompile e2) in
+	  let kk = mk_integer k 
+	  and dd = mk_integer d in
+	  let rhs = mk_plus (mk_times eq2 kk) dd in
+	  let state_eq = mk_eq eq1 rhs in
+	  let tac = scalar_norm_add [P_APP 2] e2.body in
+	  tclTHENS 
+	    (cut (mk_gt dd zero)) 
+	    [ tclTHENS (cut (mk_gt kk dd)) 
+		[tclTHENLIST [
+		  (intros_using [aux2;aux1]);
+		  (generalize_tac 
+		    [mkApp (Lazy.force coq_OMEGA4, 
+                      [| dd;kk;eq2;mkVar aux1; mkVar aux2 |])]);
+		  (clear [aux1;aux2]);
+		  (unfold sp_not);
+		  (intros_using [aux]);
+		  (resolve_id aux);
+		  (mk_then tac);
+		  assumption ] ;
+		 tclTHENLIST [
+		   (unfold sp_Zgt);
+		   simpl_in_concl; 
+		   reflexivity ] ];
+              tclTHENLIST [
+		(unfold sp_Zgt);
+                simpl_in_concl;
+		reflexivity ] ]
+      | EXACT_DIVIDE (e1,k) :: l ->
+	  let id = hyp_of_tag e1.id in
+	  let e2 =  map_eq_afine (fun c -> c / k) e1 in
+	  let eq1 = val_of(decompile e1) 
+	  and eq2 = val_of(decompile e2) in
+	  let kk = mk_integer k in
+	  let state_eq = mk_eq eq1 (mk_times eq2 kk) in
+	  if e1.kind = DISE then
+            let tac = scalar_norm [P_APP 3] e2.body in
+            tclTHENS 
+	      (cut state_eq) 
+	      [tclTHENLIST [
+		(intros_using [aux1]);
+		(generalize_tac 
+		  [mkApp (Lazy.force coq_OMEGA18, 
+                    [| eq1;eq2;kk;mkVar aux1; mkVar id |])]);
+		(clear [aux1;id]);
+		(intros_using [id]);
+		(loop l) ];
+	       tclTHEN (mk_then tac) reflexivity ]
+	  else
+            let tac = scalar_norm [P_APP 3] e2.body in
+            tclTHENS (cut state_eq) 
+	      [
+		tclTHENS 
+		 (cut (mk_gt kk zero)) 
+		 [tclTHENLIST [
+		   (intros_using [aux2;aux1]);
+		   (generalize_tac 
+		     [mkApp (Lazy.force coq_OMEGA3, 
+		       [| eq1; eq2; kk; mkVar aux2; mkVar aux1;mkVar id|])]);
+		   (clear [aux1;aux2;id]);
+		   (intros_using [id]);
+		   (loop l) ];
+		  tclTHENLIST [
+		    (unfold sp_Zgt);
+                    simpl_in_concl;
+		    reflexivity ] ];
+		tclTHEN (mk_then tac) reflexivity ]
+      | (MERGE_EQ(e3,e1,e2)) :: l ->
+	  let id = new_identifier () in
+	  tag_hypothesis id e3;
+	  let id1 = hyp_of_tag e1.id 
+	  and id2 = hyp_of_tag e2 in
+	  let eq1 = val_of(decompile e1) 
+	  and eq2 = val_of (decompile (negate_eq e1)) in
+	  let tac = 
+	    clever_rewrite [P_APP 3] [[P_APP 1]] 
+	      (Lazy.force coq_fast_Zopp_one) ::
+            scalar_norm [P_APP 3] e1.body 
+	  in
+	  tclTHENS 
+	    (cut (mk_eq eq1 (mk_inv eq2))) 
+	    [tclTHENLIST [
+	      (intros_using [aux]);
+	      (generalize_tac [mkApp (Lazy.force coq_OMEGA8, 
+	        [| eq1;eq2;mkVar id1;mkVar id2; mkVar aux|])]);
+	      (clear [id1;id2;aux]);
+	      (intros_using [id]);
+	      (loop l) ];
+            tclTHEN (mk_then tac) reflexivity]
+	    
+      | STATE(new_eq,def,orig,m,sigma) :: l ->
+	  let id = new_identifier () 
+	  and id2 = hyp_of_tag orig.id in
+	  tag_hypothesis id new_eq.id;
+	  let eq1 = val_of(decompile def) 
+	  and eq2 = val_of(decompile orig) in
+	  let vid = unintern_id sigma in
+	  let theorem =
+            mkApp (build_coq_ex (), [| 
+		      Lazy.force coq_Z;
+		      mkLambda
+			(Name vid,
+			 Lazy.force coq_Z,
+			 mk_eq (mkRel 1) eq1) |])
+	  in
+	  let mm = mk_integer m in
+	  let p_initial = [P_APP 2;P_TYPE] in
+	  let r = mk_plus eq2 (mk_times (mk_plus (mk_inv (mkVar vid)) eq1) mm) in
+	  let tac = 
+            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
+	  tclTHENS 
+	    (cut theorem)  
+	    [tclTHENLIST [
+	      (intros_using [aux]);
+	      (elim_id aux);
+	      (clear [aux]);
+	      (intros_using [vid; aux]);
+	      (generalize_tac
+		[mkApp (Lazy.force coq_OMEGA9, 
+		  [| mkVar vid;eq2;eq1;mm; mkVar id2;mkVar aux |])]);
+	      (mk_then tac);
+	      (clear [aux]);
+	      (intros_using [id]);
+	      (loop l) ];
+            tclTHEN (exists_tac eq1) reflexivity ]
+      | SPLIT_INEQ(e,(e1,act1),(e2,act2)) :: l ->
+	  let id1 = new_identifier () 
+	  and id2 = new_identifier () in
+	  tag_hypothesis id1 e1; tag_hypothesis id2 e2;
+	  let id = hyp_of_tag e.id in
+	  let tac1 = norm_add [P_APP 2;P_TYPE] e.body in
+	  let tac2 = scalar_norm_add [P_APP 2;P_TYPE] e.body in
+	  let eq = val_of(decompile e) in
+	  tclTHENS 
+	    (simplest_elim (applist (Lazy.force coq_OMEGA19, [eq; mkVar id])))
+	    [tclTHENLIST [ (mk_then tac1); (intros_using [id1]); (loop act1) ];
+             tclTHENLIST [ (mk_then tac2); (intros_using [id2]); (loop act2) ]]
+      | SUM(e3,(k1,e1),(k2,e2)) :: l ->
+	  let id = new_identifier () in
+	  tag_hypothesis id e3;
+	  let id1 = hyp_of_tag e1.id 
+	  and id2 = hyp_of_tag e2.id in
+	  let eq1 = val_of(decompile e1) 
+	  and eq2 = val_of(decompile e2) in
+	  if k1 = 1 & e2.kind = EQUA then
+            let tac_thm =
+              match e1.kind with
+		| EQUA -> Lazy.force coq_OMEGA5 
+		| INEQ -> Lazy.force coq_OMEGA6 
+		| DISE -> Lazy.force coq_OMEGA20 
+	    in
+            let kk = mk_integer k2 in
+            let p_initial =
+              if e1.kind=DISE then [P_APP 1; P_TYPE] else [P_APP 2; P_TYPE] in
+            let tac = shuffle_mult_right p_initial e1.body k2 e2.body in
+            tclTHENLIST [ 
+	      (generalize_tac
+                [mkApp (tac_thm, [| eq1; eq2; kk; mkVar id1; mkVar id2 |])]);
+	      (mk_then tac);
+	      (intros_using [id]);
+	      (loop l)
+            ]
+	  else
+            let kk1 = mk_integer k1 
+	    and kk2 = mk_integer k2 in
+	    let p_initial = [P_APP 2;P_TYPE] in
+	    let tac= shuffle_mult p_initial k1 e1.body k2 e2.body in
+            tclTHENS (cut (mk_gt kk1 zero)) 
+	      [tclTHENS 
+		 (cut (mk_gt kk2 zero)) 
+		 [tclTHENLIST [
+		   (intros_using [aux2;aux1]);
+		   (generalize_tac
+		     [mkApp (Lazy.force coq_OMEGA7, [| 
+		       eq1;eq2;kk1;kk2; 
+		       mkVar aux1;mkVar aux2;
+		       mkVar id1;mkVar id2 |])]);
+		   (clear [aux1;aux2]);
+		   (mk_then tac);
+		   (intros_using [id]);
+		   (loop l) ];
+		 tclTHENLIST [
+		   (unfold sp_Zgt);
+                   simpl_in_concl;
+		   reflexivity ] ];
+	      tclTHENLIST [
+		(unfold sp_Zgt);
+                simpl_in_concl; 
+		reflexivity ] ]
+      | CONSTANT_NOT_NUL(e,k) :: l -> 
+	  tclTHEN (generalize_tac [mkVar (hyp_of_tag e)]) Equality.discrConcl
+      | CONSTANT_NUL(e) :: l -> 
+	  tclTHEN (resolve_id (hyp_of_tag e)) reflexivity
+      | CONSTANT_NEG(e,k) :: l ->
+	  tclTHENLIST [
+	    (generalize_tac [mkVar (hyp_of_tag e)]);
+            (unfold sp_Zle);
+	    simpl_in_concl;
+	    (unfold sp_not);
+	    (intros_using [aux]);
+	    (resolve_id aux);
+	    reflexivity 
+          ]
+      | _ -> tclIDTAC 
+  in
+  loop
+
+let normalize p_initial t =
+  let (tac,t') = transform p_initial t in
+  let (tac',t'') = condense p_initial t' in
+  let (tac'',t''') = clear_zero p_initial t'' in 
+  tac @ tac' @ tac'' , t'''
+    
+let normalize_equation id flag theorem pos t t1 t2 (tactic,defs) =
+  let p_initial = [P_APP pos ;P_TYPE] in
+  let (tac,t') = normalize p_initial t in
+  let shift_left = 
+    tclTHEN 
+      (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ])
+      (tclTRY (clear [id]))
+  in
+  if tac <> [] then
+    let id' = new_identifier () in 
+    ((id',(tclTHENLIST [ (shift_left); (mk_then tac); (intros_using [id']) ]))
+          :: tactic,
+     compile id' flag t' :: defs)
+  else 
+    (tactic,defs)
+    
+let destructure_omega gl tac_def (id,c) =
+  if atompart_of_id id = "State" then 
+    tac_def
+  else
+    try match destructurate_prop c with
+      | Kapp(Eq,[typ;t1;t2]) 
+	when destructurate_type (pf_nf gl typ) = Kapp(Z,[]) ->
+	  let t = mk_plus t1 (mk_inv t2) in
+	  normalize_equation 
+	    id EQUA (Lazy.force coq_Zegal_left) 2 t t1 t2 tac_def
+      | Kapp(Zne,[t1;t2]) ->
+	  let t = mk_plus t1 (mk_inv t2) in
+	  normalize_equation
+	    id DISE (Lazy.force coq_Zne_left) 1 t t1 t2 tac_def
+      | Kapp(Zle,[t1;t2]) ->
+	  let t = mk_plus t2 (mk_inv t1) in
+	  normalize_equation
+	    id INEQ (Lazy.force coq_Zle_left) 2 t t1 t2 tac_def
+      | Kapp(Zlt,[t1;t2]) ->
+	  let t = mk_plus (mk_plus t2 (mk_integer (-1))) (mk_inv t1) in
+	  normalize_equation
+	    id INEQ (Lazy.force coq_Zlt_left) 2 t t1 t2 tac_def
+      | Kapp(Zge,[t1;t2]) ->
+	  let t = mk_plus t1 (mk_inv t2) in
+	  normalize_equation
+	    id INEQ (Lazy.force coq_Zge_left) 2 t t1 t2 tac_def
+      | Kapp(Zgt,[t1;t2]) ->
+	  let t = mk_plus (mk_plus t1 (mk_integer (-1))) (mk_inv t2) in
+	  normalize_equation
+	    id INEQ (Lazy.force coq_Zgt_left) 2 t t1 t2 tac_def
+      | _ -> tac_def
+    with e when catchable_exception e -> tac_def
+
+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 = 
+    List.fold_left (destructure_omega gl) ([],[]) (pf_hyps_types gl) in
+  let prelude,sys = 
+    List.fold_left 
+      (fun (tac,sys) (t,(v,th,b)) ->
+	 if b then
+           let id = new_identifier () in
+           let i = new_id () in
+           tag_hypothesis id i;
+           (tclTHENLIST [
+	     (simplest_elim (applist (Lazy.force coq_intro_Z, [t])));
+	     (intros_using [v; id]);
+	     (elim_id id);
+	     (clear [id]);
+	     (intros_using [th;id]);
+	     tac ]),
+           {kind = INEQ; 
+	    body = [{v=intern_id v; c=1}]; 
+            constant = 0; id = i} :: sys
+	 else
+           (tclTHENLIST [
+	     (simplest_elim (applist (Lazy.force coq_new_var, [t])));
+	     (intros_using [v;th]);
+	     tac ]),
+           sys)
+      (tclIDTAC,[]) (dump_tables ())
+  in
+  let system = system @ sys in
+  if !display_system_flag then display_system system;
+  if !old_style_flag then begin
+    try let _ = simplify false system in tclIDTAC gl
+    with UNSOLVABLE -> 
+      let _,path = depend [] [] (history ()) in
+      if !display_action_flag then display_action 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; 
+      (tclTHEN prelude (replay_history tactic_normalisation path)) gl
+    with NO_CONTRADICTION -> error "Omega can't solve this system"
+  end
+
+let coq_omega = solver_time coq_omega
+
+let nat_inject gl =
+  let aux = id_of_string "auxiliary" in
+  let table = Hashtbl.create 7 in
+  let rec explore p t = 
+    try match destructurate_term t with
+      | Kapp(Plus,[t1;t2]) ->
+          tclTHENLIST [ 
+	    (clever_rewrite_gen p (mk_plus (mk_inj t1) (mk_inj t2))
+              ((Lazy.force coq_inj_plus),[t1;t2]));
+	    (explore (P_APP 1 :: p) t1);
+	    (explore (P_APP 2 :: p) t2)
+          ]
+      | Kapp(Mult,[t1;t2]) ->
+          tclTHENLIST [
+	    (clever_rewrite_gen p (mk_times (mk_inj t1) (mk_inj t2))
+              ((Lazy.force coq_inj_mult),[t1;t2]));
+	    (explore (P_APP 1 :: p) t1);
+	    (explore (P_APP 2 :: p) t2)
+          ]
+      | Kapp(Minus,[t1;t2]) ->
+          let id = new_identifier () in
+          tclTHENS
+            (tclTHEN 
+	       (simplest_elim (applist (Lazy.force coq_le_gt_dec, [t2;t1]))) 
+	       (intros_using [id])) 
+	    [
+	      tclTHENLIST [
+	        (clever_rewrite_gen p 
+		  (mk_minus (mk_inj t1) (mk_inj t2))
+                  ((Lazy.force coq_inj_minus1),[t1;t2;mkVar id]));
+		(loop [id,mkApp (Lazy.force coq_le, [| t2;t1 |])]);
+		(explore (P_APP 1 :: p) t1);
+		(explore (P_APP 2 :: p) t2) ];
+	      (tclTHEN 
+		 (clever_rewrite_gen p (mk_integer 0)
+                    ((Lazy.force coq_inj_minus2),[t1;t2;mkVar id]))
+		 (loop [id,mkApp (Lazy.force coq_gt, [| t2;t1 |])]))
+	    ]
+      | Kapp(S,[t']) ->
+          let rec is_number t =
+            try match destructurate_term t with 
+		Kapp(S,[t]) -> is_number t
+              | Kapp(O,[]) -> true
+              | _ -> false
+            with e when catchable_exception e -> false 
+	  in
+          let rec loop p t =
+            try match destructurate_term t with 
+		Kapp(S,[t]) ->
+                  (tclTHEN 
+                     (clever_rewrite_gen p 
+			(mkApp (Lazy.force coq_Zs, [| mk_inj t |]))
+			((Lazy.force coq_inj_S),[t])) 
+		     (loop (P_APP 1 :: p) t))
+              | _ -> explore p t 
+            with e when catchable_exception e -> explore p t 
+	  in
+          if is_number t' then focused_simpl p else loop p t
+      | Kapp(Pred,[t]) ->
+          let t_minus_one = 
+	    mkApp (Lazy.force coq_minus, [| t; 
+		      mkApp (Lazy.force coq_S, [| Lazy.force coq_O |]) |]) in
+          tclTHEN
+            (clever_rewrite_gen_nat (P_APP 1 :: p) t_minus_one 
+               ((Lazy.force coq_pred_of_minus),[t]))
+            (explore p t_minus_one) 
+      | Kapp(O,[]) -> focused_simpl p
+      | _ -> tclIDTAC 
+    with e when catchable_exception e -> tclIDTAC 
+	
+  and loop = function
+    | [] -> tclIDTAC
+    | (i,t)::lit -> 
+	  begin try match destructurate_prop t with 
+              Kapp(Le,[t1;t2]) ->
+		tclTHENLIST [
+		  (generalize_tac 
+		    [mkApp (Lazy.force coq_inj_le, [| t1;t2;mkVar i |]) ]);
+		  (explore [P_APP 1; P_TYPE] t1);
+		  (explore [P_APP 2; P_TYPE] t2);
+		  (reintroduce i);
+		  (loop lit)
+                ]
+            | Kapp(Lt,[t1;t2]) ->
+		tclTHENLIST [
+		  (generalize_tac 
+		    [mkApp (Lazy.force coq_inj_lt, [| t1;t2;mkVar i |]) ]);
+		  (explore [P_APP 1; P_TYPE] t1);
+		  (explore [P_APP 2; P_TYPE] t2);
+		  (reintroduce i);
+		  (loop lit)
+                ]
+            | Kapp(Ge,[t1;t2]) ->
+		tclTHENLIST [
+		  (generalize_tac 
+		    [mkApp (Lazy.force coq_inj_ge, [| t1;t2;mkVar i |]) ]);
+		  (explore [P_APP 1; P_TYPE] t1);
+		  (explore [P_APP 2; P_TYPE] t2);
+		  (reintroduce i);
+		  (loop lit)
+                ]
+            | Kapp(Gt,[t1;t2]) ->
+		tclTHENLIST [
+		  (generalize_tac
+                    [mkApp (Lazy.force coq_inj_gt, [| t1;t2;mkVar i |]) ]);
+		  (explore [P_APP 1; P_TYPE] t1);
+		  (explore [P_APP 2; P_TYPE] t2);
+		  (reintroduce i);
+		  (loop lit)
+                ]
+            | Kapp(Neq,[t1;t2]) ->
+		tclTHENLIST [
+		  (generalize_tac
+		    [mkApp (Lazy.force coq_inj_neq, [| t1;t2;mkVar i |]) ]);
+		  (explore [P_APP 1; P_TYPE] t1);
+		  (explore [P_APP 2; P_TYPE] t2);
+		  (reintroduce i);
+		  (loop lit)
+                ]
+            | Kapp(Eq,[typ;t1;t2]) ->
+		if pf_conv_x gl typ (Lazy.force coq_nat) then
+                  tclTHENLIST [
+		    (generalize_tac 
+		      [mkApp (Lazy.force coq_inj_eq, [| t1;t2;mkVar i |]) ]);
+		    (explore [P_APP 2; P_TYPE] t1);
+		    (explore [P_APP 3; P_TYPE] t2);
+		    (reintroduce i);
+		    (loop lit)
+                  ]
+		else loop lit
+	    | _ -> loop lit
+	  with e when catchable_exception e -> loop lit end 
+  in
+  loop (List.rev (pf_hyps_types gl)) gl
+    
+let rec decidability gl t =
+  match destructurate_prop t with
+    | Kapp(Or,[t1;t2]) -> 
+	mkApp (Lazy.force coq_dec_or, [| t1; t2;
+		  decidability gl t1; decidability gl t2 |])
+    | Kapp(And,[t1;t2]) -> 
+	mkApp (Lazy.force coq_dec_and, [| t1; t2;
+		  decidability gl t1; decidability gl t2 |])
+    | Kimp(t1,t2) -> 
+	mkApp (Lazy.force coq_dec_imp, [| t1; t2;
+		  decidability gl t1; decidability gl t2 |])
+    | Kapp(Not,[t1]) -> mkApp (Lazy.force coq_dec_not, [| t1; 
+				    decidability gl t1 |])
+    | Kapp(Eq,[typ;t1;t2]) -> 
+	begin match destructurate_type (pf_nf gl typ) with
+          | Kapp(Z,[]) ->  mkApp (Lazy.force coq_dec_eq, [| t1;t2 |])
+          | Kapp(Nat,[]) ->  mkApp (Lazy.force coq_dec_eq_nat, [| t1;t2 |])
+          | _ -> errorlabstrm "decidability" 
+		(str "Omega: Can't solve a goal with equality on " ++ 
+		   Printer.prterm typ)
+	end
+    | Kapp(Zne,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zne, [| t1;t2 |])
+    | Kapp(Zle,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zle, [| t1;t2 |])
+    | Kapp(Zlt,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zlt, [| t1;t2 |])
+    | Kapp(Zge,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zge, [| t1;t2 |])
+    | Kapp(Zgt,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zgt, [| t1;t2 |])
+    | Kapp(Le, [t1;t2]) -> mkApp (Lazy.force coq_dec_le, [| t1;t2 |])
+    | Kapp(Lt, [t1;t2]) -> mkApp (Lazy.force coq_dec_lt, [| t1;t2 |])
+    | Kapp(Ge, [t1;t2]) -> mkApp (Lazy.force coq_dec_ge, [| t1;t2 |])
+    | Kapp(Gt, [t1;t2]) -> mkApp (Lazy.force coq_dec_gt, [| t1;t2 |])
+    | Kapp(False,[]) -> Lazy.force coq_dec_False
+    | Kapp(True,[]) -> Lazy.force coq_dec_True
+    | Kapp(Other t,_::_) -> error 
+	("Omega: Unrecognized predicate or connective: "^t)
+    | Kapp(Other t,[]) -> error ("Omega: Unrecognized atomic proposition: "^t)
+    | Kvar _ -> error "Omega: Can't solve a goal with proposition variables"
+    | _ -> error "Omega: Unrecognized proposition"
+
+let onClearedName id tac =
+  (* We cannot ensure that hyps can be cleared (because of dependencies), *)
+  (* so renaming may be necessary *)
+  tclTHEN
+    (tclTRY (clear [id]))
+    (fun gl -> 
+      let id = fresh_id [] id gl in
+      tclTHEN (introduction id) (tac id) gl)
+
+let destructure_hyps gl =
+  let rec loop = function
+    | [] -> (tclTHEN nat_inject coq_omega)
+    | (i,body,t)::lit ->
+	begin try match destructurate_prop t with
+	  | Kapp(False,[]) -> elim_id i
+          | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit
+          | Kapp(Or,[t1;t2]) ->
+              (tclTHENS 
+                (elim_id i)
+                [ onClearedName i (fun i -> (loop ((i,None,t1)::lit)));
+                  onClearedName i (fun i -> (loop ((i,None,t2)::lit))) ])
+          | Kapp(And,[t1;t2]) ->
+              tclTHENLIST [
+                (elim_id i);
+		(tclTRY (clear [i]));
+		(fun gl -> 
+		  let i1 = fresh_id [] (add_suffix i "_left") gl in
+		  let i2 = fresh_id [] (add_suffix i "_right") gl in
+		  tclTHENLIST [
+		    (introduction i1);
+		    (introduction i2);
+		    (loop ((i1,None,t1)::(i2,None,t2)::lit)) ] gl)
+	      ]
+          | Kimp(t1,t2) ->
+              if
+                is_Prop (pf_type_of gl t1) &
+                is_Prop (pf_type_of gl t2) &
+                closed0 t2
+              then
+		tclTHENLIST [
+		  (generalize_tac [mkApp (Lazy.force coq_imp_simp,
+                    [| t1; t2; decidability gl t1; mkVar i|])]);
+		  (onClearedName i (fun i ->
+		    (loop ((i,None,mk_or (mk_not t1) t2)::lit))))
+                ]
+              else
+		loop lit
+          | Kapp(Not,[t]) -> 
+              begin match destructurate_prop t with 
+		  Kapp(Or,[t1;t2]) -> 
+                    tclTHENLIST [
+		      (generalize_tac
+                        [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]);
+		      (onClearedName i (fun i ->
+                        (loop ((i,None,mk_and (mk_not t1) (mk_not t2)):: lit))))
+                    ]
+		| Kapp(And,[t1;t2]) -> 
+                    tclTHENLIST [
+		      (generalize_tac
+		        [mkApp (Lazy.force coq_not_and, [| t1; t2;
+			  decidability gl t1;mkVar i|])]);
+		      (onClearedName i (fun i ->
+                        (loop ((i,None,mk_or (mk_not t1) (mk_not t2))::lit))))
+                    ]
+		| Kimp(t1,t2) ->
+                    tclTHENLIST [
+		      (generalize_tac 
+		        [mkApp (Lazy.force coq_not_imp, [| t1; t2; 
+		          decidability gl t1;mkVar i |])]);
+		      (onClearedName i (fun i ->
+                        (loop ((i,None,mk_and t1 (mk_not t2)) :: lit))))
+                    ]
+		| Kapp(Not,[t]) ->
+                    tclTHENLIST [
+		      (generalize_tac
+			[mkApp (Lazy.force coq_not_not, [| t;
+			  decidability gl t; mkVar i |])]);
+		      (onClearedName i (fun i -> (loop ((i,None,t)::lit))))
+                    ]
+		| Kapp(Zle, [t1;t2]) ->
+                    tclTHENLIST [
+		      (generalize_tac
+                        [mkApp (Lazy.force coq_not_Zle, [| t1;t2;mkVar i|])]);
+		      (onClearedName i (fun _ -> loop lit))
+                    ]
+		| Kapp(Zge, [t1;t2]) ->
+                    tclTHENLIST [
+		      (generalize_tac
+                        [mkApp (Lazy.force coq_not_Zge, [| t1;t2;mkVar i|])]);
+		      (onClearedName i (fun _ -> loop lit))
+                    ]
+		| Kapp(Zlt, [t1;t2]) ->
+                    tclTHENLIST [
+		      (generalize_tac 
+                        [mkApp (Lazy.force coq_not_Zlt, [| t1;t2;mkVar i|])]);
+		      (onClearedName i (fun _ -> loop lit))
+                    ]
+		| Kapp(Zgt, [t1;t2]) ->
+                    tclTHENLIST [
+		      (generalize_tac
+                        [mkApp (Lazy.force coq_not_Zgt, [| t1;t2;mkVar i|])]);
+		      (onClearedName i (fun _ -> loop lit))
+                    ]
+		| Kapp(Le, [t1;t2]) ->
+                    tclTHENLIST [
+		      (generalize_tac
+                        [mkApp (Lazy.force coq_not_le, [| t1;t2;mkVar i|])]);
+		      (onClearedName i (fun _ -> loop lit))
+                    ]
+		| Kapp(Ge, [t1;t2]) ->
+                    tclTHENLIST [
+		      (generalize_tac
+                        [mkApp (Lazy.force coq_not_ge, [| t1;t2;mkVar i|])]);
+		      (onClearedName i (fun _ -> loop lit))
+                    ]
+		| Kapp(Lt, [t1;t2]) ->
+                    tclTHENLIST [
+		      (generalize_tac
+                        [mkApp (Lazy.force coq_not_lt, [| t1;t2;mkVar i|])]);
+		      (onClearedName i (fun _ -> loop lit))
+                    ]
+		| Kapp(Gt, [t1;t2]) ->
+                    tclTHENLIST [
+		      (generalize_tac
+                        [mkApp (Lazy.force coq_not_gt, [| t1;t2;mkVar i|])]);
+		      (onClearedName i (fun _ -> loop lit))
+                    ]
+		| Kapp(Eq,[typ;t1;t2]) ->
+                    if !old_style_flag then begin 
+		      match destructurate_type (pf_nf gl typ) with
+			| Kapp(Nat,_) -> 
+                            tclTHENLIST [
+			      (simplest_elim 
+				(mkApp
+                                  (Lazy.force coq_not_eq, [|t1;t2;mkVar i|])));
+			      (onClearedName i (fun _ -> loop lit))
+                            ]
+			| Kapp(Z,_) ->
+                            tclTHENLIST [
+			      (simplest_elim 
+				(mkApp
+				  (Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|])));
+			      (onClearedName i (fun _ -> loop lit))
+                            ]
+			| _ -> loop lit
+                    end else begin 
+		      match destructurate_type (pf_nf gl typ) with
+			| Kapp(Nat,_) -> 
+                               (tclTHEN 
+			       (convert_hyp_no_check
+                                  (i,body,
+				  (mkApp (Lazy.force coq_neq, [| t1;t2|]))))
+			       (loop lit))
+			| Kapp(Z,_) ->
+                               (tclTHEN 
+			       (convert_hyp_no_check
+                                  (i,body,
+				  (mkApp (Lazy.force coq_Zne, [| t1;t2|]))))
+			       (loop lit))
+			| _ -> loop lit
+                    end
+		| _ -> loop lit
+              end 
+          | _ -> loop lit 
+	with e when catchable_exception e -> loop lit
+	end 
+  in
+  loop (pf_hyps gl) gl
+
+let destructure_goal gl =
+  let concl = pf_concl gl in
+  let rec loop t =
+    match destructurate_prop t with
+      | Kapp(Not,[t]) ->
+          (tclTHEN 
+	     (tclTHEN (unfold sp_not) intro) 
+	     destructure_hyps)
+      | Kimp(a,b) -> (tclTHEN intro (loop b))
+      | Kapp(False,[]) -> destructure_hyps
+      | _ ->
+          (tclTHEN 
+	     (tclTHEN
+		(Tactics.refine 
+		   (mkApp (Lazy.force coq_dec_not_not, [| t;
+			      decidability gl t; mkNewMeta () |])))
+		intro) 
+	     (destructure_hyps)) 
+  in
+  (loop concl) gl
+
+let destructure_goal = all_time (destructure_goal)
+
+let omega_solver gl =
+  Library.check_required_library ["Coq";"omega";"Omega"];
+  let result = destructure_goal gl in 
+  (* if !display_time_flag then begin text_time (); 
+     flush Pervasives.stdout end; *)
+  result