3 files changed, 43 insertions, 38 deletions

diff --git a/plugins/funind/Recdef.v b/plugins/funind/Recdef.v
index e28c845ccc..e4671ccd12 100644
--- a/plugins/funind/Recdef.v
+++ b/plugins/funind/Recdef.v
@@ -5,6 +5,9 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+
+Require Import PeanoNat.
+
 Require Compare_dec.
 Require Wf_nat.
 
@@ -19,32 +22,29 @@ Fixpoint iter (n : nat) : (A -> A) -> A -> A :=
   end.
 End Iter.
 
-Theorem SSplus_lt : forall p p' : nat, p < S (S (p + p')).
-  intro p; intro p'; change (S p <= S (S (p + p')));
-    apply le_S; apply Gt.gt_le_S; change (p < S (p + p'));
-    apply Lt.le_lt_n_Sm; apply Plus.le_plus_l.
+Theorem le_lt_SS x y : x <= y -> x < S (S y).
+Proof.
+ intros. now apply Nat.lt_succ_r, Nat.le_le_succ_r.
 Qed.
 
-
-Theorem Splus_lt : forall p p' : nat, p' < S (p + p').
-  intro p; intro p'; change (S p' <= S (p + p'));
-    apply Gt.gt_le_S; change (p' < S (p + p')); apply Lt.le_lt_n_Sm;
-       apply Plus.le_plus_r.
+Theorem Splus_lt x y : y < S (x + y).
+Proof.
+ apply Nat.lt_succ_r. rewrite Nat.add_comm. apply Nat.le_add_r.
 Qed.
 
-Theorem le_lt_SS : forall x y, x <= y -> x < S (S y).
-intro x; intro y; intro H; change (S x <= S (S y));
-    apply le_S; apply Gt.gt_le_S; change (x < S y);
-    apply Lt.le_lt_n_Sm; exact H.
+Theorem SSplus_lt x y : x < S (S (x + y)).
+Proof.
+ apply le_lt_SS, Nat.le_add_r.
 Qed.
 
 Inductive max_type (m n:nat) : Set :=
   cmt : forall v, m <= v -> n <= v -> max_type m n.
 
-Definition max : forall m n:nat, max_type m n.
-intros m n; case (Compare_dec.le_gt_dec m n).
-intros h; exists n; [exact h | apply le_n].
-intros h; exists m; [apply le_n | apply Lt.lt_le_weak; exact h].
+Definition max m n : max_type m n.
+Proof.
+ destruct (Compare_dec.le_gt_dec m n) as [h|h].
+ - exists n; [exact h | apply le_n].
+ - exists m; [apply le_n | apply Nat.lt_le_incl; exact h].
 Defined.
 
-Definition Acc_intro_generator_function := fun A R => @Acc_intro_generator A R 100.
\ No newline at end of file
+Definition Acc_intro_generator_function := fun A R => @Acc_intro_generator A R 100.
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 38cbd0c533..1fa16a3015 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -43,9 +43,14 @@ open Indfun_common
 
 (* Ugly things which should not be here *)
 
-let coq_base_constant s =
-  Coqlib.gen_constant_in_modules "RecursiveDefinition"
-    (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s;;
+let coq_constant m s =
+  Coqlib.coq_constant "RecursiveDefinition" m s
+
+let arith_Nat = ["Arith";"PeanoNat";"Nat"]
+let arith_Lt = ["Arith";"Lt"]
+
+let coq_init_constant s =
+  Coqlib.gen_constant_in_modules "RecursiveDefinition" Coqlib.init_modules s
 
 let find_reference sl s =
   let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in
@@ -120,25 +125,25 @@ let v_id = Id.of_string "v"
 let def_id = Id.of_string "def"
 let p_id = Id.of_string "p"
 let rec_res_id = Id.of_string "rec_res";;
-let lt = function () -> (coq_base_constant "lt")
-let le = function () -> (coq_base_constant "le")
-let ex = function () -> (coq_base_constant "ex")
-let nat = function () -> (coq_base_constant "nat")
+let lt = function () -> (coq_init_constant "lt")
+let le = function () -> (coq_init_constant "le")
+let ex = function () -> (coq_init_constant "ex")
+let nat = function () -> (coq_init_constant "nat")
 let iter_ref () =  
   try find_reference ["Recdef"] "iter" 
   with Not_found -> error "module Recdef not loaded"
 let iter = function () -> (constr_of_global (delayed_force iter_ref))
-let eq = function () -> (coq_base_constant "eq")
+let eq = function () -> (coq_init_constant "eq")
 let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS")
-let le_lt_n_Sm = function () -> (coq_base_constant "le_lt_n_Sm")
-let le_trans = function () -> (coq_base_constant "le_trans")
-let le_lt_trans = function () -> (coq_base_constant "le_lt_trans")
-let lt_S_n = function () -> (coq_base_constant "lt_S_n")
-let le_n = function () -> (coq_base_constant "le_n")
+let le_lt_n_Sm = function () -> (coq_constant arith_Lt "le_lt_n_Sm")
+let le_trans = function () -> (coq_constant arith_Nat "le_trans")
+let le_lt_trans = function () -> (coq_constant arith_Nat "le_lt_trans")
+let lt_S_n = function () -> (coq_constant arith_Lt "lt_S_n")
+let le_n = function () -> (coq_init_constant "le_n")
 let coq_sig_ref = function () -> (find_reference ["Coq";"Init";"Specif"] "sig")
-let coq_O = function () -> (coq_base_constant "O")
-let coq_S = function () -> (coq_base_constant "S")
-let lt_n_O = function () -> (coq_base_constant "lt_n_O")
+let coq_O = function () -> (coq_init_constant "O")
+let coq_S = function () -> (coq_init_constant "S")
+let lt_n_O = function () -> (coq_constant arith_Nat "nlt_0_r")
 let max_ref = function () -> (find_reference ["Recdef"] "max")
 let max_constr = function () -> (constr_of_global (delayed_force max_ref))
 let coq_conj = function () -> find_reference Coqlib.logic_module_name "conj"
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 88958d0143..83f3462428 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -304,10 +304,10 @@ let coq_le = lazy (init_constant "le")
 let coq_lt = lazy (init_constant "lt")
 let coq_ge = lazy (init_constant "ge")
 let coq_gt = lazy (init_constant "gt")
-let coq_minus = lazy (init_constant "minus")
-let coq_plus = lazy (init_constant "plus")
-let coq_mult = lazy (init_constant "mult")
-let coq_pred = lazy (init_constant "pred")
+let coq_minus = lazy (init_constant "Nat.sub")
+let coq_plus = lazy (init_constant "Nat.add")
+let coq_mult = lazy (init_constant "Nat.mul")
+let coq_pred = lazy (init_constant "Nat.pred")
 let coq_nat = lazy (init_constant "nat")
 let coq_S = lazy (init_constant "S")
 let coq_O = lazy (init_constant "O")