Directory 'contrib' renamed into 'plugins', to end confusion with archive of user contribs

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

1 files changed, 0 insertions, 1824 deletions

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
deleted file mode 100644
index 535459885..000000000
--- a/contrib/omega/coq_omega.ml
+++ /dev/null
@@ -1,1824 +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)                                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* $Id$ *)
-
-open Util
-open Pp
-open Reduction
-open Proof_type
-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 Contradiction
-
-module OmegaSolver = Omega.MakeOmegaSolver (Bigint)
-open OmegaSolver
-
-(* 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
-
-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 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 "X%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 false (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 [all_occurrences, 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 init_arith_modules = init_modules @ arith_modules
-let coq_modules =
-  init_arith_modules @ [logic_dir] @ zarith_base_modules
-    @ [["Coq"; "omega"; "OmegaLemmas"]]
-
-let init_arith_constant = gen_constant_in_modules "Omega" init_arith_modules
-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_Z0 = lazy (constant "Z0")
-let coq_Zpos = lazy (constant "Zpos")
-let coq_Zneg = lazy (constant "Zneg")
-let coq_Z = lazy (constant "Z")
-let coq_comparison = lazy (constant "comparison")
-let coq_Gt = lazy (constant "Gt")
-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_Zsucc = lazy (constant "Zsucc")
-let coq_Zgt = lazy (constant "Zgt")
-let coq_Zle = lazy (constant "Zle")
-let coq_Z_of_nat = lazy (constant "Z_of_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_reverse = lazy (constant "fast_Zplus_assoc_reverse")
-let coq_fast_Zplus_assoc = lazy (constant "fast_Zplus_assoc")
-let coq_fast_Zmult_assoc_reverse = lazy (constant "fast_Zmult_assoc_reverse")
-let coq_fast_Zplus_permute = lazy (constant "fast_Zplus_permute")
-let coq_fast_Zplus_comm = lazy (constant "fast_Zplus_comm")
-let coq_fast_Zmult_comm = lazy (constant "fast_Zmult_comm")
-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_l = lazy (constant "fast_Zmult_plus_distr_l")
-let coq_fast_Zmult_opp_comm =  lazy (constant "fast_Zmult_opp_comm")
-let coq_fast_Zopp_plus_distr =   lazy (constant "fast_Zopp_plus_distr")
-let coq_fast_Zopp_mult_distr_r = lazy (constant "fast_Zopp_mult_distr_r")
-let coq_fast_Zopp_eq_mult_neg_1 =  lazy (constant "fast_Zopp_eq_mult_neg_1")
-let coq_fast_Zopp_involutive = lazy (constant "fast_Zopp_involutive")
-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_Znot_le_gt = lazy (constant "Znot_le_gt")
-let coq_Znot_lt_ge = lazy (constant "Znot_lt_ge")
-let coq_Znot_ge_lt = lazy (constant "Znot_ge_lt")
-let coq_Znot_gt_le = lazy (constant "Znot_gt_le")
-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 (init_arith_constant "le")
-let coq_lt = lazy (init_arith_constant "lt")
-let coq_ge = lazy (init_arith_constant "ge")
-let coq_gt = lazy (init_arith_constant "gt")
-let coq_minus = lazy (init_arith_constant "minus")
-let coq_plus = lazy (init_arith_constant "plus")
-let coq_mult = lazy (init_arith_constant "mult")
-let coq_pred = lazy (init_arith_constant "pred")
-let coq_nat = lazy (init_arith_constant "nat")
-let coq_S = lazy (init_arith_constant "S")
-let coq_O = lazy (init_arith_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_iff = lazy (constant "dec_iff")
-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_iff = lazy (constant "not_iff")
-let coq_not_not = lazy (constant "not_not")
-let coq_imp_simp = lazy (constant "imp_simp")
-let coq_iff = lazy (constant "iff")
-
-(* 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_Zsucc =     lazy (evaluable_ref_of_constr "Zsucc" coq_Zsucc)
-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_comparison; t1; t2 |])
-let mk_inj t = mkApp (Lazy.force coq_Z_of_nat, [| t |])
-
-let mk_integer n =
-  let rec loop n = 
-    if n =? one then Lazy.force coq_xH else 
-    mkApp((if n mod two =? zero then Lazy.force coq_xO else Lazy.force coq_xI),
-		[| loop (n/two) |])
-  in
-  if n =? zero then Lazy.force coq_Z0 
-  else mkApp ((if n >? zero then Lazy.force coq_Zpos else Lazy.force coq_Zneg),
-		 [| loop (abs n) |])
-    
-type omega_constant =
-  | Zplus | Zmult | Zminus | Zsucc | Zopp
-  | Plus | Mult | Minus | Pred | S | O
-  | Zpos | Zneg | Z0 | Z_of_nat
-  | Eq | Neq
-  | Zne | Zle | Zlt | Zge | Zgt
-  | Z | Nat
-  | And | Or | False | True | Not | Iff
-  | 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 = Lazy.force coq_iff -> Kapp (Iff, 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_Zsucc -> Kapp (Zsucc,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_Zpos -> Kapp (Zneg,args)
-    | _, [_] when c = Lazy.force coq_Zneg -> Kapp (Zpos,args)
-    | _, [] when c = Lazy.force coq_Z0 -> Kapp (Z0,args)
-    | _, [_] when c = Lazy.force coq_Z_of_nat -> Kapp (Z_of_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 -> one + two * loop t
-      | f, [t] when f = Lazy.force coq_xO -> two * loop t
-      | f, [] when f = Lazy.force coq_xH -> one
-      | _ -> failwith "not a number" 
-  in
-  match decompose_app t with 
-    | f, [t] when f = Lazy.force coq_Zpos -> loop t
-    | f, [t] when f = Lazy.force coq_Zneg -> neg (loop t)
-    | f, [] when f = Lazy.force coq_Z0 -> zero
-    | _ -> 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,k,t)) -> mkCast (loop i p c,k,t)
-      | ([], _) -> operation i t
-      | ((P_APP n :: p),  App (f,v)) ->
-	  let v' = Array.copy v in
-	  v'.(pred n) <- loop i p v'.(pred n); 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 (Pervasives.(+) i l) p v.(n); (mkFix (ln,(tys,lna,v')))
-      | ((P_BODY :: p), Prod (n,t,c)) ->
-	  (mkProd (n,t,loop (succ i) p c))
-      | ((P_BODY :: p), Lambda (n,t,c)) ->
-	  (mkLambda (n,t,loop (succ i) p c))
-      | ((P_BODY :: p), LetIn (n,b,t,c)) ->
-	  (mkLetIn (n,b,t,loop (succ i) 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.pr_lconstr 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,_,_)) -> loop p c
-    | ([], _) -> t
-    | ((P_APP n :: p),  App (f,v)) -> loop p v.(pred n)
-    | ((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.pr_lconstr 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 DEFAULTcast 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 bigint
-  | 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_string (string_of_bigint 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 (Evarutil.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_reverse)
-           :: 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_reverse)
-          :: tac, 
-          Oplus(l1, t')
-	else 
-          [clever_rewrite p [[P_APP 1];[P_APP 2]] 
-	     (Lazy.force coq_fast_Zplus_comm)],
-          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(Bigint.add t1 t2)
-    | t1,t2 ->
-	if weight t1 < weight t2 then
-          [clever_rewrite p [[P_APP 1];[P_APP 2]] 
-	     (Lazy.force coq_fast_Zplus_comm)],
-	  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 Bigint.add (Bigint.mult k1 c1) (Bigint.mult k2 c2) =? zero 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 Bigint.add c1 (Bigint.mult k2 c2) =? zero 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_reverse) ::
-          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_reverse) ::
-        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 >? zero 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_l) :: 
-      (tac1 @ tac2), Oplus(t1',t2')
-  | Oinv t ->
-      [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] 
-	 (Lazy.force coq_fast_Zmult_opp_comm);
-       focused_simpl (P_APP 2 :: p)], Otimes(t,Oz(neg 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_reverse);
-       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_reverse) ::
-	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_plus_distr) :: 
-      (tac1 @ tac2),
-      Oplus(t1',t2')
-  | Oinv t ->
-      [clever_rewrite p [[P_APP 1;P_APP 1]] (Lazy.force coq_fast_Zopp_involutive)], 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_mult_distr_r);
-       focused_simpl (P_APP 2 :: p)], Otimes(t1,Oz (neg x))
-  | Otimes(t1,t2) -> error "Omega: Can't solve a goal with non-linear products"
-  | (Oatom _ as t) ->
-      let r = Otimes(t,Oz(negone)) in
-      [clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1)], r
-  | Oz i -> [focused_simpl p],Oz(neg i)
-  | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zopp, [| c |]))
-      
-let rec transform p t = 
-  let default isnat t' =
-    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 isnat;
-      [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(Zsucc,[t1]) ->
-	let tac,t = transform p (mkApp (Lazy.force coq_Zplus,
-					 [| t1; mk_integer one |])) in
-	unfold sp_Zsucc :: 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_comm) in
-             let tac,t' = scalar p n t2' in tac1 @ tac2 @ (sym :: tac),t'
-         | _ -> default false t
-       end
-   | Kapp((Zpos|Zneg|Z0),_) -> 
-       (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(Z_of_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
-    | Oatom v,Oatom _ -> 
-	let r = Otimes(Oatom v,Oz two) 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 one)) 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 one)) 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 one) 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) -> Bigint.add (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) 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) -> 
-      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 zero) 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 n),r) when n =? zero ->
-      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 izero = mk_integer zero 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 negone else one 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 not_sup_sup = mkApp (build_coq_eq (), [| 
-					Lazy.force coq_comparison; 
-					Lazy.force coq_Gt;
-					Lazy.force coq_Gt |])
-	    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 izero)) 
-		    [ 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 c = floor_div e1.constant k in
-	  let d = Bigint.sub e1.constant (Bigint.mult c k) in
-	  let e2 =  {id=e1.id; kind=EQUA;constant = c; 
-                     body = map_eq_linear (fun c -> c / k) e1.body } in
-	  let eq2 = val_of(decompile e2) in
-	  let kk = mk_integer k 
-	  and dd = mk_integer d in
-	  let tac = scalar_norm_add [P_APP 2] e2.body in
-	  tclTHENS 
-	    (cut (mk_gt dd izero)) 
-	    [ 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 izero)) 
-		 [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_eq_mult_neg_1) ::
-            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 {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 e.id;
-	  let eq1 = val_of(decompile def) 
-	  and eq2 = val_of(decompile orig) in
-	  let vid = unintern_id v 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 tac = 
-            clever_rewrite (P_APP 1 :: P_APP 1 :: P_APP 2 :: p_initial) 
-              [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1) ::
-            shuffle_mult_right p_initial
-              orig.body m ({c= negone;v= v}::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 (inj_open 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 =? one & 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 izero)) 
-	      [tclTHENS 
-		 (cut (mk_gt kk2 izero)) 
-		 [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 negone)) (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 negone)) (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=one}]; 
-            constant = zero; 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 display_var system;
-  if !old_style_flag then begin
-    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 display_var path;
-      (tclTHEN prelude (replay_history tactic_normalisation path)) gl 
-  end else begin 
-    try
-      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
-
-let coq_omega = solver_time coq_omega
-
-let nat_inject gl =
-  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 zero)
-                    ((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_Zsucc, [| 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 |])
-    | Kapp(Iff,[t1;t2]) -> 
-	mkApp (Lazy.force coq_dec_iff, [| 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.pr_lconstr 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)
-	      ]
-          | Kapp(Iff,[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;
-		    generalize_tac
-		      [mkApp (Lazy.force coq_imp_simp,
-                        [| t1; t2; decidability gl t1; mkVar i1|])];
-		    onClearedName i1 (fun i1 ->
-		      tclTHENLIST [
-			introduction i2;
-			generalize_tac
-			  [mkApp (Lazy.force coq_imp_simp,
-                            [| t2; t1; decidability gl t2; mkVar i2|])];
-			onClearedName i2 (fun i2 ->
-			  loop
-			  ((i1,None,mk_or (mk_not t1) t2)::
-			   (i2,None,mk_or (mk_not t2) t1)::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))))
-                    ]
-		| Kapp(Iff,[t1;t2]) ->
-                    tclTHENLIST [
-		      (generalize_tac
-		        [mkApp (Lazy.force coq_not_iff, [| t1; t2;
-			  decidability gl t1; decidability gl t2; mkVar i|])]);
-		      (onClearedName i (fun i ->
-                        (loop ((i,None,
-			        mk_or (mk_and t1 (mk_not t2))
-				      (mk_and (mk_not t1) 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_Znot_le_gt, [| t1;t2;mkVar i|])]);
-		      (onClearedName i (fun _ -> loop lit))
-                    ]
-		| Kapp(Zge, [t1;t2]) ->
-                    tclTHENLIST [
-		      (generalize_tac
-                        [mkApp (Lazy.force coq_Znot_ge_lt, [| t1;t2;mkVar i|])]);
-		      (onClearedName i (fun _ -> loop lit))
-                    ]
-		| Kapp(Zlt, [t1;t2]) ->
-                    tclTHENLIST [
-		      (generalize_tac 
-                        [mkApp (Lazy.force coq_Znot_lt_ge, [| t1;t2;mkVar i|])]);
-		      (onClearedName i (fun _ -> loop lit))
-                    ]
-		| Kapp(Zgt, [t1;t2]) ->
-                    tclTHENLIST [
-		      (generalize_tac
-                        [mkApp (Lazy.force coq_Znot_gt_le, [| 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 =
-  Coqlib.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