Beginning of a reorganisation of the ml part for romega:

 - deletion of some dead code
 - grouping all stuff depending on Z in a nice module Int



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

3 files changed, 379 insertions, 175 deletions

diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml
index 4853c10f5..90d6c584e 100644
--- a/contrib/romega/const_omega.ml
+++ b/contrib/romega/const_omega.ml
@@ -48,64 +48,16 @@ let dest_const_apply t =
     | _ -> raise Destruct
   in  Nametab.id_of_global ref, args
 
-let recognize_number t =
-  let rec loop t =
-    let f,l = dest_const_apply t in
-    match Names.string_of_id f,l with
-       "xI",[t] -> Bigint.add Bigint.one (Bigint.mult Bigint.two (loop t))
-     | "xO",[t] -> Bigint.mult Bigint.two (loop t)
-     | "xH",[] -> Bigint.one
-     | _ -> failwith "not a number" in
-  let f,l = dest_const_apply t in
-    match Names.string_of_id f,l with
-        "Zpos",[t] -> loop t
-      | "Zneg",[t] -> Bigint.neg (loop t)
-      | "Z0",[] -> Bigint.zero
-      | _ -> failwith "not a number";;
-
-
 let logic_dir = ["Coq";"Logic";"Decidable"]
 
 let coq_modules =
   Coqlib.init_modules @ [logic_dir] @ Coqlib.arith_modules @ Coqlib.zarith_base_modules
-    @ [["Coq"; "omega"; "OmegaLemmas"]]
     @ [["Coq"; "Lists"; "List"]]
     @ [module_refl_path]
     @ [module_refl_path@["ZOmega"]]
 
 let constant = Coqlib.gen_constant_in_modules "Omega" coq_modules
 
-let coq_xH = lazy (constant "xH")
-let coq_xO = lazy (constant "xO")
-let coq_xI = lazy (constant "xI")
-let coq_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_Lt = lazy (constant "Lt")
-let coq_Eq = lazy (constant "Eq")
-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")
-
-(* Peano *)
-let coq_le = lazy(constant "le")
-let coq_gt = lazy(constant "gt")
-
-(* Integers *)
-let coq_nat = lazy(constant "nat")
-let coq_S = lazy(constant "S")
-let coq_O = lazy(constant "O")
-let coq_minus = lazy(constant "minus")
-
 (* Logic *)
 let coq_eq = lazy(constant  "eq")
 let coq_refl_equal = lazy(constant  "refl_equal")
@@ -114,13 +66,8 @@ let coq_not = lazy(constant "not")
 let coq_or = lazy(constant "or")
 let coq_True = lazy(constant "True")
 let coq_False = lazy(constant "False")
-let coq_ex = lazy(constant "ex")
 let coq_I = lazy(constant "I")
 
-(* Lists *)
-let coq_cons =  lazy (constant "cons")
-let coq_nil =  lazy (constant "nil")
-
 (* ReflOmegaCore/ZOmega *)
 
 let coq_h_step = lazy (constant "h_step")
@@ -138,6 +85,7 @@ let coq_t_opp = lazy (constant  "Topp")
 let coq_t_minus = lazy (constant  "Tminus")
 let coq_t_var = lazy (constant  "Tvar")
 
+let coq_proposition = lazy (constant  "proposition")
 let coq_p_eq = lazy (constant  "EqTerm")
 let coq_p_leq = lazy (constant  "LeqTerm")
 let coq_p_geq = lazy (constant  "GeqTerm")
@@ -152,14 +100,6 @@ let coq_p_and = lazy (constant  "Tand")
 let coq_p_imp = lazy (constant  "Timp")
 let coq_p_prop = lazy (constant  "Tprop")
 
-let coq_proposition = lazy (constant  "proposition")
-let coq_interp_sequent = lazy (constant  "interp_goal_concl")
-let coq_normalize_sequent = lazy (constant  "normalize_goal")
-let coq_execute_sequent = lazy (constant  "execute_goal")
-let coq_do_concl_to_hyp =  lazy (constant  "do_concl_to_hyp")
-let coq_sequent_to_hyps = lazy (constant  "goal_to_hyps")
-let coq_normalize_hyps_goal = lazy (constant  "normalize_hyps_goal")
-
 (* Constructors for shuffle tactic *)
 let coq_t_fusion =  lazy (constant  "t_fusion")
 let coq_f_equal =  lazy (constant  "F_equal")
@@ -194,8 +134,7 @@ let coq_c_red4 = lazy (constant  "C_RED4")
 let coq_c_red5 = lazy (constant  "C_RED5")
 let coq_c_red6 = lazy (constant  "C_RED6")
 let coq_c_mult_opp_left = lazy (constant  "C_MULT_OPP_LEFT")
-let coq_c_mult_assoc_reduced = 
-  lazy (constant  "C_MULT_ASSOC_REDUCED")
+let coq_c_mult_assoc_reduced = lazy (constant  "C_MULT_ASSOC_REDUCED")
 let coq_c_minus = lazy (constant  "C_MINUS")
 let coq_c_mult_comm = lazy (constant  "C_MULT_COMM")
 
@@ -223,30 +162,11 @@ let coq_e_split = lazy  (constant  "E_SPLIT")
 let coq_e_extract = lazy  (constant  "E_EXTRACT")
 let coq_e_solve = lazy  (constant  "E_SOLVE")
 
-let coq_decompose_solve_valid = 
-  lazy (constant   "decompose_solve_valid")
-let coq_do_reduce_lhyps = lazy (constant   "do_reduce_lhyps")
+let coq_interp_sequent = lazy (constant  "interp_goal_concl")
 let coq_do_omega = lazy (constant  "do_omega")
 
 (* \subsection{Construction d'expressions} *)
 
-
-let mk_var v = Term.mkVar (Names.id_of_string v)
-let mk_plus t1 t2 = Term.mkApp (Lazy.force coq_Zplus,[|  t1; t2 |])
-let mk_times t1 t2 = Term.mkApp (Lazy.force coq_Zmult, [| t1; t2 |])
-let mk_minus t1 t2 = Term.mkApp (Lazy.force coq_Zminus, [| t1;t2 |])
-let mk_eq t1 t2 = Term.mkApp (Lazy.force coq_eq, [| Lazy.force coq_Z; t1; t2 |])
-let mk_le t1 t2 = Term.mkApp (Lazy.force coq_Zle, [|t1; t2 |])
-let mk_gt t1 t2 = Term.mkApp (Lazy.force coq_Zgt, [|t1; t2 |])
-let mk_inv t = Term.mkApp (Lazy.force coq_Zopp, [|t |])
-let mk_and t1 t2 =  Term.mkApp (Lazy.force coq_and, [|t1; t2 |])
-let mk_or t1 t2 =  Term.mkApp (Lazy.force coq_or, [|t1; t2 |])
-let mk_not t = Term.mkApp (Lazy.force coq_not, [|t |])
-let mk_eq_rel t1 t2 = Term.mkApp (Lazy.force coq_eq, [|
-				Lazy.force coq_comparison; t1; t2 |])
-let mk_inj t = Term.mkApp (Lazy.force coq_Z_of_nat, [|t |])
-
-
 let do_left t = 
   if t = Lazy.force coq_c_nop then Lazy.force coq_c_nop
   else Term.mkApp (Lazy.force coq_c_do_left, [|t |] )
@@ -270,27 +190,20 @@ let rec do_list = function
   | [x] -> x
   | (x::l) -> do_seq x (do_list l)
 
-let mk_integer n =
-  let rec loop n = 
-    if n=Bigint.one then Lazy.force coq_xH else
-      let (q,r) = Bigint.euclid n Bigint.two in
-      Term.mkApp
-        ((if r = Bigint.zero then Lazy.force coq_xO else Lazy.force coq_xI),
-	[| loop q |]) in
-    
-    if n = Bigint.zero then Lazy.force coq_Z0 
-    else
-      if Bigint.is_strictly_pos n then
-        Term.mkApp (Lazy.force coq_Zpos, [| loop n |])
-      else
-        Term.mkApp (Lazy.force coq_Zneg, [| loop (Bigint.neg n) |])
+(* Nat *)
 
-let mk_Z = mk_integer
+let coq_S = lazy(constant "S")
+let coq_O = lazy(constant "O")
 
 let rec mk_nat = function
   | 0 -> Lazy.force coq_O
   | n -> Term.mkApp (Lazy.force coq_S, [| mk_nat (n-1) |])
 
+(* Lists *)
+
+let coq_cons =  lazy (constant "cons")
+let coq_nil =  lazy (constant "nil")
+
 let mk_list typ l =
   let rec loop = function
     | [] ->
@@ -303,3 +216,136 @@ let mk_plist l = mk_list Term.mkProp l
 
 let mk_shuffle_list l = mk_list (Lazy.force coq_t_fusion) l
 
+
+type parse_term = 
+  | Tplus of Term.constr * Term.constr 
+  | Tmult of Term.constr * Term.constr
+  | Tminus of Term.constr * Term.constr
+  | Topp of Term.constr
+  | Tsucc of Term.constr
+  | Tnum of Bigint.bigint
+  | Tother 
+
+type parse_rel = 
+  | Req of Term.constr * Term.constr
+  | Rne of Term.constr * Term.constr
+  | Rlt of Term.constr * Term.constr
+  | Rle of Term.constr * Term.constr
+  | Rgt of Term.constr * Term.constr
+  | Rge of Term.constr * Term.constr
+  | Rtrue
+  | Rfalse
+  | Rnot of Term.constr
+  | Ror of Term.constr * Term.constr
+  | Rand of Term.constr * Term.constr
+  | Rimp of Term.constr * Term.constr
+  | Riff of Term.constr * Term.constr
+  | Rother
+
+let parse_logic_rel c = 
+ try match destructurate c with
+   | Kapp("True",[]) -> Rtrue
+   | Kapp("False",[]) -> Rfalse
+   | Kapp("not",[t]) -> Rnot t
+   | Kapp("or",[t1;t2]) -> Ror (t1,t2) 
+   | Kapp("and",[t1;t2]) -> Rand (t1,t2)
+   | Kimp(t1,t2) -> Rimp (t1,t2)
+   | Kapp("iff",[t1;t2]) -> Riff (t1,t2)
+   | _ -> Rother
+ with e when Logic.catchable_exception e -> Rother
+
+
+module type Int = sig
+  val typ : Term.constr Lazy.t
+  val plus : Term.constr Lazy.t 
+  val mult : Term.constr Lazy.t
+  val opp : Term.constr Lazy.t
+  val minus : Term.constr Lazy.t
+
+  val mk : Bigint.bigint -> Term.constr
+  val parse_term : Term.constr -> parse_term
+  val parse_rel : Proof_type.goal Tacmach.sigma -> Term.constr -> parse_rel
+  (* check whether t is built only with numbers and + * - *)
+  val is_scalar : Term.constr -> bool 
+end
+
+module Z : Int = struct 
+
+let typ = lazy (constant "Z")
+let plus = lazy (constant "Zplus")
+let mult = lazy (constant  "Zmult")
+let opp = lazy (constant "Zopp")
+let minus = lazy (constant "Zminus")
+
+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 recognize t =
+  let rec loop t =
+    let f,l = dest_const_apply t in
+    match Names.string_of_id f,l with
+       "xI",[t] -> Bigint.add Bigint.one (Bigint.mult Bigint.two (loop t))
+     | "xO",[t] -> Bigint.mult Bigint.two (loop t)
+     | "xH",[] -> Bigint.one
+     | _ -> failwith "not a number" in
+  let f,l = dest_const_apply t in
+    match Names.string_of_id f,l with
+        "Zpos",[t] -> loop t
+      | "Zneg",[t] -> Bigint.neg (loop t)
+      | "Z0",[] -> Bigint.zero
+      | _ -> failwith "not a number";;
+
+let rec mk_positive n = 
+  if n=Bigint.one then Lazy.force coq_xH 
+  else
+    let (q,r) = Bigint.euclid n Bigint.two in
+    Term.mkApp
+      ((if r = Bigint.zero then Lazy.force coq_xO else Lazy.force coq_xI),
+       [| mk_positive q |]) 
+
+let mk_Z n =
+  if n = Bigint.zero then Lazy.force coq_Z0 
+  else if Bigint.is_strictly_pos n then
+    Term.mkApp (Lazy.force coq_Zpos, [| mk_positive n |])
+  else
+    Term.mkApp (Lazy.force coq_Zneg, [| mk_positive (Bigint.neg n) |])
+
+let mk = mk_Z
+
+let parse_term t = 
+  try match destructurate t with
+    | Kapp("Zplus",[t1;t2]) -> Tplus (t1,t2)
+    | Kapp("Zminus",[t1;t2]) -> Tminus (t1,t2)
+    | Kapp("Zmult",[t1;t2]) -> Tmult (t1,t2)
+    | Kapp("Zopp",[t]) -> Topp t
+    | Kapp("Zsucc",[t]) -> Tsucc t
+    | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> 
+	(try Tnum (recognize t) with _ -> Tother)
+    | _ -> Tother
+  with e when Logic.catchable_exception e -> Tother
+    
+let parse_rel gl t = 
+  try match destructurate t with 
+    | Kapp("eq",[typ;t1;t2]) 
+      when destructurate (Tacmach.pf_nf gl typ) = Kapp("Z",[]) -> Req (t1,t2)
+    | Kapp("Zne",[t1;t2]) -> Rne (t1,t2)
+    | Kapp("Zle",[t1;t2]) -> Rle (t1,t2)
+    | Kapp("Zlt",[t1;t2]) -> Rlt (t1,t2)
+    | Kapp("Zge",[t1;t2]) -> Rge (t1,t2)
+    | Kapp("Zgt",[t1;t2]) -> Rgt (t1,t2)
+    | _ -> parse_logic_rel t 
+  with e when Logic.catchable_exception e -> Rother
+
+let is_scalar t =
+  let rec aux t = match destructurate t with
+    | Kapp(("Zplus"|"Zminus"|"Zmult"),[t1;t2]) -> aux t1 & aux t2
+    | Kapp(("Zopp"|"Zsucc"),[t]) -> aux t
+    | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> let _ = recognize t in true
+    | _ -> false in
+  try aux t with _ -> false
+
+end
diff --git a/contrib/romega/const_omega.mli b/contrib/romega/const_omega.mli
new file mode 100644
index 000000000..04b26463a
--- /dev/null
+++ b/contrib/romega/const_omega.mli
@@ -0,0 +1,179 @@
+(*************************************************************************
+
+   PROJET RNRT Calife - 2001
+   Author: Pierre Crégut - France Télécom R&D
+   Licence : LGPL version 2.1
+
+ *************************************************************************)
+
+
+(** Coq objects used in romega *)
+
+(* from Logic *)
+val coq_eq : Term.constr lazy_t
+val coq_refl_equal : Term.constr lazy_t
+val coq_and : Term.constr lazy_t
+val coq_not : Term.constr lazy_t
+val coq_or : Term.constr lazy_t
+val coq_True : Term.constr lazy_t
+val coq_False : Term.constr lazy_t
+val coq_I : Term.constr lazy_t
+
+(* from ReflOmegaCore/ZOmega *)
+val coq_h_step : Term.constr lazy_t
+val coq_pair_step : Term.constr lazy_t
+val coq_p_left : Term.constr lazy_t
+val coq_p_right : Term.constr lazy_t
+val coq_p_invert : Term.constr lazy_t
+val coq_p_step : Term.constr lazy_t
+val coq_p_nop : Term.constr lazy_t
+
+val coq_t_int : Term.constr lazy_t
+val coq_t_plus : Term.constr lazy_t
+val coq_t_mult : Term.constr lazy_t
+val coq_t_opp : Term.constr lazy_t
+val coq_t_minus : Term.constr lazy_t
+val coq_t_var : Term.constr lazy_t
+
+val coq_proposition : Term.constr lazy_t
+val coq_p_eq : Term.constr lazy_t
+val coq_p_leq : Term.constr lazy_t
+val coq_p_geq : Term.constr lazy_t
+val coq_p_lt : Term.constr lazy_t
+val coq_p_gt : Term.constr lazy_t
+val coq_p_neq : Term.constr lazy_t
+val coq_p_true : Term.constr lazy_t
+val coq_p_false : Term.constr lazy_t
+val coq_p_not : Term.constr lazy_t
+val coq_p_or : Term.constr lazy_t
+val coq_p_and : Term.constr lazy_t
+val coq_p_imp : Term.constr lazy_t
+val coq_p_prop : Term.constr lazy_t
+
+val coq_t_fusion : Term.constr lazy_t
+val coq_f_equal : Term.constr lazy_t
+val coq_f_cancel : Term.constr lazy_t
+val coq_f_left : Term.constr lazy_t
+val coq_f_right : Term.constr lazy_t
+
+val coq_step : Term.constr lazy_t
+val coq_c_do_both : Term.constr lazy_t
+val coq_c_do_left : Term.constr lazy_t
+val coq_c_do_right : Term.constr lazy_t
+val coq_c_do_seq : Term.constr lazy_t
+val coq_c_nop : Term.constr lazy_t
+val coq_c_opp_plus : Term.constr lazy_t
+val coq_c_opp_opp : Term.constr lazy_t
+val coq_c_opp_mult_r : Term.constr lazy_t
+val coq_c_opp_one : Term.constr lazy_t
+val coq_c_reduce : Term.constr lazy_t
+val coq_c_mult_plus_distr : Term.constr lazy_t
+val coq_c_opp_left : Term.constr lazy_t
+val coq_c_mult_assoc_r : Term.constr lazy_t
+val coq_c_plus_assoc_r : Term.constr lazy_t
+val coq_c_plus_assoc_l : Term.constr lazy_t
+val coq_c_plus_permute : Term.constr lazy_t
+val coq_c_plus_comm : Term.constr lazy_t
+val coq_c_red0 : Term.constr lazy_t
+val coq_c_red1 : Term.constr lazy_t
+val coq_c_red2 : Term.constr lazy_t
+val coq_c_red3 : Term.constr lazy_t
+val coq_c_red4 : Term.constr lazy_t
+val coq_c_red5 : Term.constr lazy_t
+val coq_c_red6 : Term.constr lazy_t
+val coq_c_mult_opp_left : Term.constr lazy_t
+val coq_c_mult_assoc_reduced : Term.constr lazy_t
+val coq_c_minus : Term.constr lazy_t
+val coq_c_mult_comm : Term.constr lazy_t
+
+val coq_s_constant_not_nul : Term.constr lazy_t
+val coq_s_constant_neg : Term.constr lazy_t
+val coq_s_div_approx : Term.constr lazy_t
+val coq_s_not_exact_divide : Term.constr lazy_t
+val coq_s_exact_divide : Term.constr lazy_t
+val coq_s_sum : Term.constr lazy_t
+val coq_s_state : Term.constr lazy_t
+val coq_s_contradiction : Term.constr lazy_t
+val coq_s_merge_eq : Term.constr lazy_t
+val coq_s_split_ineq : Term.constr lazy_t
+val coq_s_constant_nul : Term.constr lazy_t
+val coq_s_negate_contradict : Term.constr lazy_t
+val coq_s_negate_contradict_inv : Term.constr lazy_t
+
+val coq_direction : Term.constr lazy_t
+val coq_d_left : Term.constr lazy_t
+val coq_d_right : Term.constr lazy_t
+val coq_d_mono : Term.constr lazy_t
+
+val coq_e_split : Term.constr lazy_t
+val coq_e_extract : Term.constr lazy_t
+val coq_e_solve : Term.constr lazy_t
+val coq_interp_sequent : Term.constr lazy_t
+val coq_do_omega : Term.constr lazy_t
+
+(** Building expressions *)
+
+val do_left : Term.constr -> Term.constr
+val do_right : Term.constr -> Term.constr
+val do_both : Term.constr -> Term.constr -> Term.constr
+val do_seq : Term.constr -> Term.constr -> Term.constr
+val do_list : Term.constr list -> Term.constr
+
+val mk_nat : int -> Term.constr
+val mk_list : Term.constr -> Term.constr list -> Term.constr
+val mk_plist : Term.types list -> Term.types
+val mk_shuffle_list : Term.constr list -> Term.constr
+
+(** Analyzing a coq term *)
+
+(* The generic result shape of the analysis of a term.
+   One-level depth, except when a number is found *)
+type parse_term =
+    Tplus of Term.constr * Term.constr
+  | Tmult of Term.constr * Term.constr
+  | Tminus of Term.constr * Term.constr
+  | Topp of Term.constr
+  | Tsucc of Term.constr
+  | Tnum of Bigint.bigint
+  | Tother
+
+(* The generic result shape of the analysis of a relation.
+   One-level depth. *)
+type parse_rel =
+    Req of Term.constr * Term.constr
+  | Rne of Term.constr * Term.constr
+  | Rlt of Term.constr * Term.constr
+  | Rle of Term.constr * Term.constr
+  | Rgt of Term.constr * Term.constr
+  | Rge of Term.constr * Term.constr
+  | Rtrue
+  | Rfalse
+  | Rnot of Term.constr
+  | Ror of Term.constr * Term.constr
+  | Rand of Term.constr * Term.constr
+  | Rimp of Term.constr * Term.constr
+  | Riff of Term.constr * Term.constr
+  | Rother
+
+(* A module factorizing what we should now about the number representation *)
+module type Int =
+  sig
+    (* the coq type of the numbers *)
+    val typ : Term.constr Lazy.t
+    (* the operations on the numbers *)
+    val plus : Term.constr Lazy.t
+    val mult : Term.constr Lazy.t
+    val opp : Term.constr Lazy.t
+    val minus : Term.constr Lazy.t
+    (* building a coq number *)
+    val mk : Bigint.bigint -> Term.constr
+    (* parsing a term (one level, except if a number is found) *)
+    val parse_term : Term.constr -> parse_term
+    (* parsing a relation expression, including = < <= >= > *)
+    val parse_rel : Proof_type.goal Tacmach.sigma -> Term.constr -> parse_rel
+    (* Is a particular term only made of numbers and + * - ? *) 
+    val is_scalar : Term.constr -> bool
+  end
+
+(* Currently, we only use Z numbers *)
+module Z : Int
diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml
index 7c99f7e14..fc4f7a8f0 100644
--- a/contrib/romega/refl_omega.ml
+++ b/contrib/romega/refl_omega.ml
@@ -301,13 +301,6 @@ let omega_of_oformula env kind =
 
 (* \subsection{Omega vers Oformula} *)
 
-let reified_of_atom env i =
-  try Hashtbl.find env.real_indices i
-  with Not_found -> 
-    Printf.printf "Atome %d non trouvé\n" i; 
-    Hashtbl.iter (fun k v -> Printf.printf "%d -> %d\n" k v) env.real_indices;
-    raise Not_found
-
 let rec oformula_of_omega env af = 
   let rec loop = function
     | ({v=v; c=n}::r) ->
@@ -321,20 +314,27 @@ let app f v = mkApp(Lazy.force f,v)
 
 let rec coq_of_formula env t =
   let rec loop = function
-  | Oplus (t1,t2) -> app coq_Zplus [| loop t1; loop t2 |]
-  | Oopp t -> app coq_Zopp [| loop t |]
-  | Omult(t1,t2) -> app coq_Zmult [| loop t1; loop t2 |]
-  | Oint v ->   mk_Z v
+  | Oplus (t1,t2) -> app Z.plus [| loop t1; loop t2 |]
+  | Oopp t -> app Z.opp [| loop t |]
+  | Omult(t1,t2) -> app Z.mult [| loop t1; loop t2 |]
+  | Oint v ->   Z.mk v
   | Oufo t -> loop t
   | Oatom var ->
       (* attention ne traite pas les nouvelles variables si on ne les
        * met pas dans env.term *)
       get_reified_atom env var
-  | Ominus(t1,t2) -> app coq_Zminus [| loop t1; loop t2 |] in
+  | Ominus(t1,t2) -> app Z.minus [| loop t1; loop t2 |] in
   loop t
 
 (* \subsection{Oformula vers COQ reifié} *)
 
+let reified_of_atom env i =
+  try Hashtbl.find env.real_indices i
+  with Not_found -> 
+    Printf.printf "Atome %d non trouvé\n" i; 
+    Hashtbl.iter (fun k v -> Printf.printf "%d -> %d\n" k v) env.real_indices;
+    raise Not_found
+
 let rec reified_of_formula env = function
   | Oplus (t1,t2) ->
       app coq_t_plus [| reified_of_formula env t1; reified_of_formula env t2 |]
@@ -342,7 +342,7 @@ let rec reified_of_formula env = function
       app coq_t_opp [| reified_of_formula env t |]
   | Omult(t1,t2) ->
       app coq_t_mult [| reified_of_formula env t1; reified_of_formula env t2 |]
-  | Oint v ->  app coq_t_int [| mk_Z v |]
+  | Oint v ->  app coq_t_int [| Z.mk v |]
   | Oufo t -> reified_of_formula env t
   | Oatom i -> app coq_t_var [| mk_nat (reified_of_atom env i) |]
   | Ominus(t1,t2) ->
@@ -387,12 +387,12 @@ let reified_of_proposition env f =
 
 let reified_of_omega env body constant = 
   let coeff_constant = 
-    app coq_t_int [| mk_Z constant |] in
+    app coq_t_int [| Z.mk constant |] in
   let mk_coeff {c=c; v=v} t =
     let coef = 
       app coq_t_mult 
 	[| reified_of_formula env (unintern_omega env v); 
-	   app coq_t_int [| mk_Z c |] |] in
+	   app coq_t_int [| Z.mk c |] |] in
     app coq_t_plus [|coef; t |] in
   List.fold_right mk_coeff body coeff_constant
 
@@ -666,36 +666,23 @@ let normalize_equation env (negated,depends,origin,path) (oper,t1,t2) =
 
 (* \section{Compilation des hypothèses} *)
 
-let is_scalar t =
-  let rec aux t = match destructurate t with
-    | Kapp(("Zplus"|"Zminus"|"Zmult"),[t1;t2]) -> aux t1 & aux t2
-    | Kapp(("Zopp"|"Zsucc"),[t]) -> aux t
-    | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> let _ = recognize_number t in true
-    | _ -> false in
-  try aux t with _ -> false
-
 let rec oformula_of_constr env t =
-  try match destructurate t with
-  | Kapp("Zplus",[t1;t2]) -> binop env (fun x y -> Oplus(x,y)) t1 t2
-  | Kapp("Zminus",[t1;t2]) -> binop env (fun x y -> Ominus(x,y)) t1 t2
-  | Kapp("Zmult",[t1;t2]) when is_scalar t1 or is_scalar t2 ->
-      binop env (fun x y -> Omult(x,y)) t1 t2
-  | Kapp("Zopp",[t]) -> Oopp(oformula_of_constr env t)
-  | Kapp("Zsucc",[t]) -> Oplus(oformula_of_constr env t, Oint one)
-  | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> 
-      begin try Oint(recognize_number t)
-      with _ -> Oatom (add_reified_atom t env) end
-  | _ -> 
-      Oatom (add_reified_atom t env)
-  with e when Logic.catchable_exception e ->
-    Oatom (add_reified_atom t env)
-
-and  binop env c t1 t2 = 
-    let t1' = oformula_of_constr env t1 in
-    let t2' = oformula_of_constr env t2 in
-    c t1' t2'
-
-and  binprop env (neg2,depends,origin,path) 
+  match Z.parse_term t with 
+    | Tplus (t1,t2) -> binop env (fun x y -> Oplus(x,y)) t1 t2
+    | Tminus (t1,t2) -> binop env (fun x y -> Ominus(x,y)) t1 t2
+    | Tmult (t1,t2) when Z.is_scalar t1 || Z.is_scalar t2 -> 
+	binop env (fun x y -> Omult(x,y)) t1 t2
+    | Topp t -> Oopp(oformula_of_constr env t)
+    | Tsucc t -> Oplus(oformula_of_constr env t, Oint one)
+    | Tnum n -> Oint n
+    | _ -> Oatom (add_reified_atom t env)
+
+and binop env c t1 t2 = 
+  let t1' = oformula_of_constr env t1 in
+  let t2' = oformula_of_constr env t2 in
+  c t1' t2'
+
+and binprop env (neg2,depends,origin,path) 
              add_to_depends neg1 gl c t1 t2 =
   let i = new_connector_id env in
   let depends1 = if add_to_depends then Left i::depends else depends in
@@ -718,40 +705,32 @@ and mk_equation env ctxt c connector t1 t2 =
   Pequa (c,omega)
 
 and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c = 
-  try match destructurate c with
-    | Kapp("eq",[typ;t1;t2]) 
-      when destructurate (Tacmach.pf_nf gl typ) = Kapp("Z",[]) ->
-         mk_equation env ctxt c Eq t1 t2
-    | Kapp("Zne",[t1;t2]) -> 
-	mk_equation env ctxt c Neq t1 t2
-    | Kapp("Zle",[t1;t2]) -> 
-	mk_equation env ctxt c Leq t1 t2
-    | Kapp("Zlt",[t1;t2]) -> 
-	mk_equation env ctxt c Lt t1 t2
-    | Kapp("Zge",[t1;t2]) -> 
-	mk_equation env ctxt c Geq t1 t2
-    | Kapp("Zgt",[t1;t2]) -> 
-	mk_equation env ctxt c Gt t1 t2
-    | Kapp("True",[]) -> Ptrue
-    | Kapp("False",[]) -> Pfalse
-    | Kapp("not",[t]) ->
-       let t' = 
-	 oproposition_of_constr 
-	   env (not negated, depends, origin,(O_mono::path)) gl t in 
-       Pnot t'
-    | Kapp("or",[t1;t2]) ->  
+  match Z.parse_rel gl c with 
+    | Req (t1,t2) -> mk_equation env ctxt c Eq t1 t2
+    | Rne (t1,t2) -> mk_equation env ctxt c Neq t1 t2
+    | Rle (t1,t2) -> mk_equation env ctxt c Leq t1 t2
+    | Rlt (t1,t2) -> mk_equation env ctxt c Lt t1 t2
+    | Rge (t1,t2) -> mk_equation env ctxt c Geq t1 t2
+    | Rgt (t1,t2) -> mk_equation env ctxt c Gt t1 t2
+    | Rtrue -> Ptrue 
+    | Rfalse -> Pfalse
+    | Rnot t -> 
+	let t' = 
+	  oproposition_of_constr 
+	    env (not negated, depends, origin,(O_mono::path)) gl t in 
+	Pnot t'
+    | Ror (t1,t2) -> 
 	binprop env ctxt (not negated) negated gl (fun i x y -> Por(i,x,y)) t1 t2
-    | Kapp("and",[t1;t2]) ->
+    | Rand (t1,t2) -> 
 	binprop env ctxt negated negated gl
 	  (fun i x y -> Pand(i,x,y)) t1 t2
-    | Kimp(t1,t2) ->
+    | Rimp (t1,t2) ->
 	binprop env ctxt (not negated) (not negated) gl 
 	  (fun i x y -> Pimp(i,x,y)) t1 t2
-    | Kapp("iff",[t1;t2]) ->
+    | Riff (t1,t2) ->
 	binprop env ctxt negated negated gl 
 	  (fun i x y -> Pand(i,x,y)) (Term.mkArrow t1 t2) (Term.mkArrow t2 t1)
     | _ -> Pprop c
-  with e when Logic.catchable_exception e -> Pprop c
 
 (* Destructuration des hypothèses et de la conclusion *)
 
@@ -918,7 +897,7 @@ let add_stated_equations env tree =
     let coq_v = coq_of_formula env v_def in
     let v = add_reified_atom coq_v env in
     (* Le terme qu'il va falloir introduire *)
-    let term_to_generalize = app coq_refl_equal [|Lazy.force coq_Z; coq_v|] in
+    let term_to_generalize = app coq_refl_equal [|Lazy.force Z.typ; coq_v|] in
     (* sa représentation sous forme d'équation mais non réifié car on n'a pas
      * l'environnement pour le faire correctement *)
     let term_to_reify = (v_def,Oatom v) in
@@ -1064,7 +1043,7 @@ let replay_history env env_hyp =
 		    mk_nat (get_hyp env_hyp e2.id) |])
       | DIVIDE_AND_APPROX (e1,e2,k,d) :: l ->
 	  mkApp (Lazy.force coq_s_div_approx,
-		 [| mk_Z k; mk_Z d; 
+		 [| Z.mk k; Z.mk d; 
 		    reified_of_omega env e2.body e2.constant;
 		    mk_nat (List.length e2.body); 
 		    loop env_hyp l; mk_nat (get_hyp env_hyp e1.id) |])
@@ -1073,7 +1052,7 @@ let replay_history env env_hyp =
 	  let d = e1.constant - e2_constant * k in
 	  let e2_body = map_eq_linear (fun c -> c / k) e1.body in
           mkApp (Lazy.force coq_s_not_exact_divide,
-		 [|mk_Z k; mk_Z d; 
+		 [|Z.mk k; Z.mk d; 
 		   reified_of_omega env e2_body e2_constant; 
 		   mk_nat (List.length e2_body); 
 		   mk_nat (get_hyp env_hyp e1.id)|])
@@ -1082,7 +1061,7 @@ let replay_history env env_hyp =
 	    map_eq_linear (fun c -> c / k) e1.body in
 	  let e2_constant = floor_div e1.constant k in
           mkApp (Lazy.force coq_s_exact_divide,
-		 [|mk_Z k; 
+		 [|Z.mk k; 
 		   reified_of_omega env e2_body e2_constant; 
 		   mk_nat (List.length e2_body);
 		   loop env_hyp l; mk_nat (get_hyp env_hyp e1.id)|])
@@ -1097,7 +1076,7 @@ let replay_history env env_hyp =
 	  and n2 = get_hyp env_hyp e2.id in
 	  let trace = shuffle_path k1 e1.body k2 e2.body in
           mkApp (Lazy.force coq_s_sum,
-		 [| mk_Z k1; mk_nat n1; mk_Z k2;
+		 [| Z.mk k1; mk_nat n1; Z.mk k2;
 		    mk_nat n2; trace; (loop (CCEqua e3 :: env_hyp) l) |])
       | CONSTANT_NOT_NUL(e,k) :: l -> 
           mkApp (Lazy.force coq_s_constant_not_nul,
@@ -1117,7 +1096,7 @@ let replay_history env env_hyp =
 	     Oplus (o_orig,Omult (Oplus (Oopp v,o_def), Oint m)) in
           let trace,_ = normalize_linear_term env body in
 	  mkApp (Lazy.force coq_s_state,
-		 [| mk_Z m; trace; mk_nat n1; mk_nat n2; 
+		 [| Z.mk m; trace; mk_nat n1; mk_nat n2; 
 		    loop (CCEqua new_eq.id :: env_hyp) l |])
       |	HYP _ :: l -> loop env_hyp l
       |	CONSTANT_NUL e :: l ->
@@ -1243,7 +1222,7 @@ let resolution env full_reified_goal systems_list =
 	  Hashtbl.add env.real_indices var i; t :: loop (succ i) l
       |	[] -> [] in
     loop 0 all_vars_env in
-  let env_terms_reified = mk_list (Lazy.force coq_Z) basic_env in
+  let env_terms_reified = mk_list (Lazy.force Z.typ) basic_env in
   (* On peut maintenant généraliser le but : env est a jour *)
   let l_reified_stated =
      List.map (fun (_,_,(l,r),_) ->