Ajout lemmes arithmetiques

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

1 files changed, 29 insertions, 23 deletions

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 6c8badb5f..15022750a 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -229,6 +229,7 @@ let constant dir s =
 	     (Nametab.string_of_qualid (Nametab.make_qualid dir id)))
 
 let zarith_constant dir = constant ("Zarith"::dir)
+let logic_constant dir = constant ("Logic"::dir)
 
 (* fast_integer *)
 let coq_xH = lazy (zarith_constant ["fast_integer"] "xH")
@@ -314,42 +315,21 @@ let coq_Zlt_left = lazy (zarith_constant ["auxiliary"] "Zlt_left")
 let coq_Zge_left = lazy (zarith_constant ["auxiliary"] "Zge_left")
 let coq_Zgt_left = lazy (zarith_constant ["auxiliary"] "Zgt_left")
 let coq_Zle_left = lazy (zarith_constant ["auxiliary"] "Zle_left")
-let coq_eq_ind_r = lazy (zarith_constant ["auxiliary"] "eq_ind_r")
 let coq_new_var = lazy (zarith_constant ["auxiliary"] "new_var")
 let coq_intro_Z = lazy (zarith_constant ["auxiliary"] "intro_Z")
-let coq_dec_or = lazy (zarith_constant ["auxiliary"] "dec_or")
-let coq_dec_and = lazy (zarith_constant ["auxiliary"] "dec_and")
-let coq_dec_imp = lazy (zarith_constant ["auxiliary"] "dec_imp")
-let coq_dec_not = lazy (zarith_constant ["auxiliary"] "dec_not")
-let coq_dec_eq_nat = lazy (zarith_constant ["auxiliary"] "dec_eq_nat")
+
 let coq_dec_eq = lazy (zarith_constant ["auxiliary"] "dec_eq")
 let coq_dec_Zne = lazy (zarith_constant ["auxiliary"] "dec_Zne")
 let coq_dec_Zle = lazy (zarith_constant ["auxiliary"] "dec_Zle")
 let coq_dec_Zlt = lazy (zarith_constant ["auxiliary"] "dec_Zlt")
 let coq_dec_Zgt = lazy (zarith_constant ["auxiliary"] "dec_Zgt")
 let coq_dec_Zge = lazy (zarith_constant ["auxiliary"] "dec_Zge")
-let coq_dec_le = lazy (zarith_constant ["auxiliary"] "dec_le")
-let coq_dec_lt = lazy (zarith_constant ["auxiliary"] "dec_lt")
-let coq_dec_ge = lazy (zarith_constant ["auxiliary"] "dec_ge")
-let coq_dec_gt = lazy (zarith_constant ["auxiliary"] "dec_gt")
-let coq_dec_False = lazy (zarith_constant ["auxiliary"] "dec_False")
-let coq_dec_not_not = lazy (zarith_constant ["auxiliary"] "dec_not_not")
-let coq_dec_True = lazy (zarith_constant ["auxiliary"] "dec_True")
+
 let coq_not_Zeq = lazy (zarith_constant ["auxiliary"] "not_Zeq")
 let coq_not_Zle = lazy (zarith_constant ["auxiliary"] "not_Zle")
 let coq_not_Zlt = lazy (zarith_constant ["auxiliary"] "not_Zlt")
 let coq_not_Zge = lazy (zarith_constant ["auxiliary"] "not_Zge")
 let coq_not_Zgt = lazy (zarith_constant ["auxiliary"] "not_Zgt")
-let coq_not_le = lazy (zarith_constant ["auxiliary"] "not_le")
-let coq_not_lt = lazy (zarith_constant ["auxiliary"] "not_lt")
-let coq_not_ge = lazy (zarith_constant ["auxiliary"] "not_ge")
-let coq_not_gt = lazy (zarith_constant ["auxiliary"] "not_gt")
-let coq_not_eq = lazy (zarith_constant ["auxiliary"] "not_eq")
-let coq_not_or = lazy (zarith_constant ["auxiliary"] "not_or")
-let coq_not_and = lazy (zarith_constant ["auxiliary"] "not_and")
-let coq_not_imp = lazy (zarith_constant ["auxiliary"] "not_imp")
-let coq_not_not = lazy (zarith_constant ["auxiliary"] "not_not")
-let coq_imp_simp = lazy (zarith_constant ["auxiliary"] "imp_simp")
 let coq_neq = lazy (zarith_constant ["auxiliary"] "neq")
 let coq_Zne = lazy (zarith_constant ["auxiliary"] "Zne")
 
@@ -367,10 +347,36 @@ let coq_minus = lazy (constant ["Arith";"Minus"] "minus")
 
 (* Compare_dec *)
 let coq_le_gt_dec = lazy (constant ["Arith";"Compare_dec"] "le_gt_dec")
+let coq_dec_eq_nat = lazy (constant ["Arith";"Peano_dec"] "dec_eq_nat")
+let coq_dec_le = lazy (constant ["Arith";"Compare_dec"] "dec_le")
+let coq_dec_lt = lazy (constant ["Arith";"Compare_dec"] "dec_lt")
+let coq_dec_ge = lazy (constant ["Arith";"Compare_dec"] "dec_ge")
+let coq_dec_gt = lazy (constant ["Arith";"Compare_dec"] "dec_gt")
+let coq_not_eq = lazy (constant ["Arith";"Compare_dec"] "not_eq")
+let coq_not_le = lazy (constant ["Arith";"Compare_dec"] "not_le")
+let coq_not_lt = lazy (constant ["Arith";"Compare_dec"] "not_lt")
+let coq_not_ge = lazy (constant ["Arith";"Compare_dec"] "not_ge")
+let coq_not_gt = lazy (constant ["Arith";"Compare_dec"] "not_gt")
 
 (* Logic *)
 open Coqlib
 let build_coq_eq = build_coq_eq_data.eq
+let coq_eq_ind_r = lazy (constant ["Init"; "Logic"] "eq_ind_r")
+
+let coq_dec_or = lazy (logic_constant ["Decidable"] "dec_or")
+let coq_dec_and = lazy (logic_constant ["Decidable"] "dec_and")
+let coq_dec_imp = lazy (logic_constant ["Decidable"] "dec_imp")
+let coq_dec_not = lazy (logic_constant ["Decidable"] "dec_not")
+let coq_dec_False = lazy (logic_constant ["Decidable"] "dec_False")
+let coq_dec_not_not = lazy (logic_constant ["Decidable"] "dec_not_not")
+let coq_dec_True = lazy (logic_constant ["Decidable"] "dec_True")
+
+let coq_not_or = lazy (logic_constant ["Decidable"] "not_or")
+let coq_not_and = lazy (logic_constant ["Decidable"] "not_and")
+let coq_not_imp = lazy (logic_constant ["Decidable"] "not_imp")
+let coq_not_not = lazy (logic_constant ["Decidable"] "not_not")
+let coq_imp_simp = lazy (logic_constant ["Decidable"] "imp_simp")
+
 (* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *)